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