Theorem: nat=>beubyte11s*-injectivity
(defthm nat=>beubyte11s*-injectivity (equal (equal (nat=>beubyte11s* nat1) (nat=>beubyte11s* nat2)) (equal (nfix nat1) (nfix nat2))))