Rules about compustatep.
There are other rules that involve compustatep elsewhere, but we also need the rule here, which does not readily fit elsewhere. At some point we may improve the organization of the symbolic execution rules.
Theorem:
(defthm compustatep-of-if*-when-both-compustatep (implies (and (compustatep b) (compustatep c)) (compustatep (if* a b c))))