Theorem: nat=>bebits-of-bebits=>nat
(defthm nat=>bebits-of-bebits=>nat (equal (nat=>bebits (len digits) (bebits=>nat digits)) (bit-list-fix digits)))