Theorems about fsubcor-var.
Theorem:
(defthm pseudo-termp-of-fsubcor-var (implies (and (pseudo-term-listp terms) (pseudo-termp form)) (pseudo-termp (fsubcor-var vars terms form))))
Theorem:
(defthm pseudo-term-listp-of-fsubcor-var-lst (implies (and (pseudo-term-listp terms) (pseudo-term-listp forms)) (pseudo-term-listp (fsubcor-var-lst vars terms forms))))