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