Turn each
(def-error-checker-x-symbols xs) → x-symbols
Function:
(defun def-error-checker-x-symbols (xs) (declare (xargs :guard (true-listp xs))) (let ((__function__ 'def-error-checker-x-symbols)) (declare (ignorable __function__)) (b* (((when (endp xs)) nil) (x (car xs)) (x-symbol (if (atom x) x (car x))) (x-symbols (def-error-checker-x-symbols (cdr xs)))) (cons x-symbol x-symbols))))
Theorem:
(defthm true-listp-of-def-error-checker-x-symbols (b* ((x-symbols (def-error-checker-x-symbols xs))) (true-listp x-symbols)) :rule-classes :rewrite)