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