Lift fact-info->thm-name to lists.
(fact-info-list->thm-name-list infos) → thm-names
Function:
(defun fact-info-list->thm-name-list (infos) (declare (xargs :guard (fact-info-listp infos))) (let ((__function__ 'fact-info-list->thm-name-list)) (declare (ignorable __function__)) (cond ((endp infos) nil) (t (cons (fact-info->thm-name (car infos)) (fact-info-list->thm-name-list (cdr infos)))))))
Theorem:
(defthm symbol-listp-of-fact-info-list->thm-name-list (implies (and (fact-info-listp infos)) (b* ((thm-names (fact-info-list->thm-name-list infos))) (symbol-listp thm-names))) :rule-classes :rewrite)