Correctness theorem for find-fun.
Theorem: find-fun-of-dead
(defthm find-fun-of-dead (equal (find-fun fun (funenv-dead funenv)) (funinfo+funenv-result-dead (find-fun fun funenv))))