Correctness theorem for ensure-funscope-disjoint.
Theorem: ensure-funscope-disjoint-of-dead
(defthm ensure-funscope-disjoint-of-dead (equal (ensure-funscope-disjoint (funscope-dead funscope) (funenv-dead funenv)) (ensure-funscope-disjoint funscope funenv)))