Lift atj-function-type->outputs to lists.
(atj-function-type-list->outputs fn-types) → out-typess
Function:
(defun atj-function-type-list->outputs (fn-types) (declare (xargs :guard (atj-function-type-listp fn-types))) (let ((__function__ 'atj-function-type-list->outputs)) (declare (ignorable __function__)) (cond ((endp fn-types) nil) (t (cons (atj-function-type->outputs (car fn-types)) (atj-function-type-list->outputs (cdr fn-types)))))))
Theorem:
(defthm atj-type-list-listp-of-atj-function-type-list->outputs (b* ((out-typess (atj-function-type-list->outputs fn-types))) (atj-type-list-listp out-typess)) :rule-classes :rewrite)