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