Theorem:
(defthm bebits=>nat-injectivity+ (implies (and (equal (trim-bendian+ (bit-list-fix digits1)) digits1) (equal (trim-bendian+ (bit-list-fix digits2)) digits2)) (equal (equal (bebits=>nat digits1) (bebits=>nat digits2)) (equal digits1 digits2))))