A strategy for proving sets are equal because they are subsets
of one another.
Double containment can be a good way to prove that two sets are
equal to one another.
Unfortunately, because this rule targets equal it can get quite
expensive. You may sometimes wish to disable it to speed up your proofs, as
directed by accumulated-persistence.
Definitions and Theorems
(implies (and (setp x) (setp y))
(equal (equal x y)
(and (subset x y) (subset y x))))
:rule-classes ((:rewrite :backchain-limit-lst 1)))