Rules about the interaction of boolean-from-sint and sint-from-boolean.
These are actually not used in the old-style big symbolic execution, but rather in the new-style modular compositional proofs.
Theorem:
(defthm boolean-from-sint-of-sint-from-boolean (implies (booleanp x) (equal (boolean-from-sint (sint-from-boolean x)) x)))