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