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