Theorem: nat=>bebytes-of-bebytes=>nat
(defthm nat=>bebytes-of-bebytes=>nat (equal (nat=>bebytes (len digits) (bebytes=>nat digits)) (byte-list-fix digits)))