Theorems about finite sets.
Note that the theorem that rewrites in to member-equal
is disabled by default.
It can be locally enabled in certain proofs as needed.
(equal (cardinality (tail x))
(if (empty x) 0 (1- (cardinality x)))))
(implies (subset x y)
(subset (tail x) y)))
(implies (setp x)
(iff (in a x) (member-equal a x))))