Low-level lemma to rewrite
This theorem is disabled by default and most users shouldn't enable it. It's only needed to prove properties about the basic sbitset constructors.
This is a little more complicated than in the basic bitset library, because we have to go to the proper pair.
Theorem:
(defthm in-of-sbitset-members (equal (in a (sbitset-members x)) (and (sbitsetp x) (let ((pair (sbitset-find (floor a *sbitset-block-size*) x))) (and pair (in a (sbitset-pair-members pair)))))))