Theorem that statements-to-fundefs is nil under statement-list-nofunp.
Theorem: statements-to-fundefs-when-nofunp
(defthm statements-to-fundefs-when-nofunp (implies (statement-list-nofunp stmts) (equal (statements-to-fundefs stmts) nil)))
