Correctness theorem for funinfo-for-fundef.
Theorem: funinfo-for-fundef-of-dead
(defthm funinfo-for-fundef-of-dead (equal (funinfo-for-fundef (fundef-dead fundef)) (funinfo-dead (funinfo-for-fundef fundef))))