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