Programmatic interface to simplify-defun
Call simplify-defun-programmatic exactly as you would call
simplify-defun, except that arguments are not automatically quoted; so
avoid using arguments of the form (:eval x). Unlike simplify-defun,
simplify-defun-programmatic does not introduce a new definition or
theorem. Rather, it returns the encapsulate form that would be evaluated
by simplify-defun — that is, the form displayed by a corresponding
call of show-simplify-defun.