Theorem: lebits=>nat-of-nat=>lebits*
(defthm lebits=>nat-of-nat=>lebits* (equal (lebits=>nat (nat=>lebits* nat)) (nfix nat)))