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