Lift atj-test-value-ACL2 to lists.
(atj-test-value-acl2-list values) → test-values
Function:
(defun atj-test-value-acl2-list (values) (declare (xargs :guard (true-listp values))) (let ((__function__ 'atj-test-value-acl2-list)) (declare (ignorable __function__)) (cond ((endp values) nil) (t (cons (atj-test-value-acl2 (car values)) (atj-test-value-acl2-list (cdr values)))))))
Theorem:
(defthm atj-test-value-listp-of-atj-test-value-acl2-list (b* ((test-values (atj-test-value-acl2-list values))) (atj-test-value-listp test-values)) :rule-classes :rewrite)