Lemmas about logite from the logops-lemmas book.
Theorem: simplify-logite
(defthm simplify-logite (and (equal (logite 0 then else) (ifix else)) (equal (logite -1 then else) (ifix then))))
