Lift atj-type-to-type-list to lists.
(atj-type-list-to-type-list-list types) → typess
Function:
(defun atj-type-list-to-type-list-list (types) (declare (xargs :guard (atj-type-listp types))) (let ((__function__ 'atj-type-list-to-type-list-list)) (declare (ignorable __function__)) (cond ((endp types) nil) (t (cons (atj-type-to-type-list (car types)) (atj-type-list-to-type-list-list (cdr types)))))))
Theorem:
(defthm atj-type-list-listp-of-atj-type-list-to-type-list-list (b* ((typess (atj-type-list-to-type-list-list types))) (atj-type-list-listp typess)) :rule-classes :rewrite)
Theorem:
(defthm cons-listp-of-atj-type-list-to-type-list-list (b* ((typess (atj-type-list-to-type-list-list types))) (cons-listp typess)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-type-list-to-type-list-list (b* ((?typess (atj-type-list-to-type-list-list types))) (equal (len typess) (len types))))
Theorem:
(defthm atj-type-list-to-type-list-list-of-atj-type-list-fix-types (equal (atj-type-list-to-type-list-list (atj-type-list-fix types)) (atj-type-list-to-type-list-list types)))
Theorem:
(defthm atj-type-list-to-type-list-list-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-type-list-to-type-list-list types) (atj-type-list-to-type-list-list types-equiv))) :rule-classes :congruence)