Theorem: nat=>bebits-injectivity
(defthm nat=>bebits-injectivity (implies (and (< (nfix nat1) (expt 2 (nfix width))) (< (nfix nat2) (expt 2 (nfix width)))) (equal (equal (nat=>bebits width nat1) (nat=>bebits width nat2)) (equal (nfix nat1) (nfix nat2)))))