Rules about boolean equalities.
We just have a fairly ad hoc rule here; since it is so ad hoc, it is not quite clear whether it is appropriate to put it into a more general library or not, so for now we leave it here.
The need for this rule arises in the modular theorems
generated for the non-strict disjunctive operator
Theorem:
(defthm equal-to-t-when-holds-and-boolean (implies (and (booleanp b) (test* b)) (equal (equal t b) t)))