Calls ensure-function-not-in-termination-thm with ctx and state as the last two arguments.
Macro: ensure-function-not-in-termination-thm$
(defmacro ensure-function-not-in-termination-thm$ (fn description error-erp error-val) (list 'ensure-function-not-in-termination-thm fn description error-erp error-val 'ctx 'state))