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