Lift atj-type-rewrap-term to lists.
(atj-type-rewrap-terms terms dst-typess) → rewrapped-terms
Function:
(defun atj-type-rewrap-terms (terms dst-typess) (declare (xargs :guard (and (pseudo-term-listp terms) (atj-type-list-listp dst-typess)))) (declare (xargs :guard (and (cons-listp dst-typess) (= (len terms) (len dst-typess))))) (let ((__function__ 'atj-type-rewrap-terms)) (declare (ignorable __function__)) (cond ((endp terms) nil) (t (cons (atj-type-rewrap-term (car terms) (car dst-typess)) (atj-type-rewrap-terms (cdr terms) (cdr dst-typess)))))))
Theorem:
(defthm pseudo-term-listp-of-atj-type-rewrap-terms (b* ((rewrapped-terms (atj-type-rewrap-terms terms dst-typess))) (pseudo-term-listp rewrapped-terms)) :rule-classes :rewrite)