Theorem: bebits=>nat-of-nat=>bebits
(defthm bebits=>nat-of-nat=>bebits (implies (< (nfix nat) (expt 2 (nfix width))) (equal (bebits=>nat (nat=>bebits width nat)) (nfix nat))))