Theorem:
(defthm beubyte11s=>nat-injectivity* (implies (and (equal (trim-bendian* (ubyte11-list-fix digits1)) digits1) (equal (trim-bendian* (ubyte11-list-fix digits2)) digits2)) (equal (equal (beubyte11s=>nat digits1) (beubyte11s=>nat digits2)) (equal digits1 digits2))))