Theorem: nat=>bebytes*-injectivity
(defthm nat=>bebytes*-injectivity (equal (equal (nat=>bebytes* nat1) (nat=>bebytes* nat2)) (equal (nfix nat1) (nfix nat2))))