Theorem: nat=>beubyte11s*-of-beubyte11s=>nat
(defthm nat=>beubyte11s*-of-beubyte11s=>nat (equal (nat=>beubyte11s* (beubyte11s=>nat digits)) (trim-bendian* (ubyte11-list-fix digits))))