(rename-ident-list idents subst) → new-idents
Function:
(defun rename-ident-list (idents subst) (declare (xargs :guard (and (ident-listp idents) (ident-ident-alistp subst)))) (declare (ignorable idents subst)) (let ((__function__ 'rename-ident-list)) (declare (ignorable __function__)) (if (endp idents) nil (cons (rename-ident (car idents) subst) (rename-ident-list (cdr idents) subst)))))
Theorem:
(defthm ident-listp-of-rename-ident-list (b* ((new-idents (rename-ident-list idents subst))) (ident-listp new-idents)) :rule-classes :rewrite)