Correctness theorem for funscope-for-fundefs.
Theorem: funscope-for-fundefs-of-dead
(defthm funscope-for-fundefs-of-dead (equal (funscope-for-fundefs (fundef-list-dead fundefs)) (funscope-result-dead (funscope-for-fundefs fundefs))))