Rules about sint-from-boolean.
Theorem:
(defthm sint-from-boolean-when-true (implies x (equal (sint-from-boolean x) (sint-from-integer 1))))
Theorem:
(defthm sint-from-boolean-when-true-test* (implies (test* x) (equal (sint-from-boolean x) (sint-from-integer 1))))
Theorem:
(defthm sint-from-boolean-when-false (implies (not x) (equal (sint-from-boolean x) (sint-from-integer 0))))
Theorem:
(defthm sint-from-boolean-when-false-test* (implies (test* (not x)) (equal (sint-from-boolean x) (sint-from-integer 0))))