FTY version of fsublis-var-lst.
(fty-fsublis-var-lst subst terms) → new-terms
Function:
(defun fty-fsublis-var-lst (subst terms) (declare (xargs :guard (and (symbol-pseudoterm-alistp subst) (pseudo-term-listp terms)))) (let ((__function__ 'fty-fsublis-var-lst)) (declare (ignorable __function__)) (fsublis-var-lst (symbol-pseudoterm-alist-fix subst) (pseudo-term-list-fix terms))))
Theorem:
(defthm pseudo-term-listp-of-fty-fsublis-var-lst (b* ((new-terms (fty-fsublis-var-lst subst terms))) (pseudo-term-listp new-terms)) :rule-classes :rewrite)