Rules about if*.
These rules are unrelated to the special status of if* in BDD reasoning. These rules are useful when if* is used as a more controllable version of the built-in if, e.g. so that ACL2 does not do unwanted case splits.
(defthm if*-when-true (implies a (equal (if* a b c) b)))
(defthm if*-when-false (implies (not a) (equal (if* a b c) c)))