Theorem about add-funs and
If add-funs is successful on a list of function definitions without nested function definitions and a function environment without function definitions in the bodies, the result is a function envnrionment without function definitions in the bodies. That is, this property of the function environment is preserved.
Theorem:
(defthm funenv-nofunp-of-add-funs (implies (and (fundef-list-nofunp fundefs) (funenv-nofunp funenv) (not (reserrp (add-funs fundefs funenv)))) (funenv-nofunp (add-funs fundefs funenv))))