Theorem: nat=>leubyte11s+-injectivity
(defthm nat=>leubyte11s+-injectivity (equal (equal (nat=>leubyte11s+ nat1) (nat=>leubyte11s+ nat2)) (equal (nfix nat1) (nfix nat2))))