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