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
Theorem:
(defthm double-containment (implies (and (setp x) (setp y)) (equal (equal x y) (and (subset x y) (subset y x)))) :rule-classes ((:rewrite :backchain-limit-lst 1)))