Relation between char and short bit sizes.
Theorem: char-bits-vs-short-bits
(defthm char-bits-vs-short-bits (< (char-bits) (short-bits)) :rule-classes ((:linear :trigger-terms ((char-bits) (short-bits)))))
