Correctness theorem for add-funs.
This is relevant for the top-level block, which has function definitions.
Theorem:
(defthm add-funs-of-dead (equal (add-funs (fundef-list-dead fundefs) (funenv-dead funenv)) (funenv-result-dead (add-funs fundefs funenv))))