Rules about boolean-from-sint.
We also have two rules
to simplify applications of boolean-from-sint
to
Theorem:
(defthm boolean-from-sint-of-0 (equal (boolean-from-sint (sint-from-integer 0)) nil))
Theorem:
(defthm boolean-from-sint-of-1 (equal (boolean-from-sint (sint-from-integer 1)) t))