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.
(defthm cardinality-of-tail (equal (cardinality (tail x)) (if (empty x) 0 (1- (cardinality x)))))
(defthm subset-of-tail-left (implies (subset x y) (subset (tail x) y)))
(defthm in-to-member-when-setp (implies (setp x) (iff (in a x) (member-equal a x))))