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