Theorem: beubyte11s=>nat-injectivity
(defthm beubyte11s=>nat-injectivity (implies (equal (len digits1) (len digits2)) (equal (equal (beubyte11s=>nat digits1) (beubyte11s=>nat digits2)) (equal (ubyte11-list-fix digits1) (ubyte11-list-fix digits2)))))