Relation between long and llong bit sizes.
Theorem: long-bits-vs-llong-bits
(defthm long-bits-vs-llong-bits (= (long-bits) (llong-bits)) :rule-classes ((:linear :trigger-terms ((long-bits) (llong-bits)))))