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