Recognize true lists of translated term functions.
(termfn-listp x wrld) → std::bool
We would need stronger world assumptions for
Function:
(defun termfn-listp (x wrld) (declare (xargs :guard (plist-worldp-with-formals wrld))) (let ((__function__ 'termfn-listp)) (declare (ignorable __function__)) (if (consp x) (and (termfnp (car x) wrld) (termfn-listp (cdr x) wrld)) (null x))))