# Double-containment

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. In fact, this rule is disabled
when importing [books]/std/osets/top.lisp. To reduce its cost when enabled,
this rule has a backchain limit.

On the other hand, there are cases in which this rule works well, and where
the backchain limit is detrimental. For this reason, we also provide a version
of the rule that has no backchain limit. This version can be enabled
as needed.

### Definitions and Theorems

**Theorem: **double-containment

(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)))

**Theorem: **double-containment-no-backchain-limit

(defthm double-containment-no-backchain-limit
(implies (and (setp x) (setp y))
(equal (equal x y)
(and (subset x y) (subset y x)))))