Theorem: bebytes=>nat-of-nat=>bebytes*
(defthm bebytes=>nat-of-nat=>bebytes* (equal (bebytes=>nat (nat=>bebytes* nat)) (nfix nat)))