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