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