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