Atc-if*-rules
Rules about if*.
We just have a fairly ad hoc rule here;
because it is so ad hoc, for now we prefer not to add it
to [books]/std/basic/if-star.lisp.
The need for this rule arises in the modular theorems
generated for the non-strict disjunctive operator ||.
Due to the fact that (or a b) is (if a a b),
with the condition repeated in the `then' branch,
and the fact that if is turned into if*
in the modular theorems generated by ATC,
a subgoal (booleanp (if* t t ...)) comes up.
This rule serves to resolve it.
Definitions and Theorems
Theorem: if*-of-t-and-t
(defthm if*-of-t-and-t
(booleanp (if* t t x)))