Rules to support proofs generated for tag declarations.
Currently we have just one rule. It is a bit odd, but it does speed up the proofs where it is used, e.g. from over 2 seconds to under 1 second.
Theorem:
(defthm atc-tag-generation-if-when-true (implies a (equal (if a b c) b)))