Carry out a strsubst replacement throughout a list of strings.

`(strsubst-list old new x)` replaces every occurrence of

Example:

(strsubst-list "Sun" "Moon" '("Sun Roof" "Hello Sun" "Sunny Sunshades")) --> ("Moon Roof" "Hello Moon" "Moonny Moonshades")

**Function: **

(defun strsubst-list (old new x) (declare (xargs :guard (and (stringp old) (stringp new) (string-listp x)))) (if (atom x) nil (cons (strsubst old new (car x)) (strsubst-list old new (cdr x)))))

**Theorem: **

(defthm strsubst-list-when-atom (implies (atom x) (equal (strsubst-list old new x) nil)))

**Theorem: **

(defthm strsubst-list-of-cons (equal (strsubst-list old new (cons a x)) (cons (strsubst old new a) (strsubst-list old new x))))

**Theorem: **

(defthm string-listp-of-strsubst-list (string-listp (strsubst-list old new x)))

**Theorem: **

(defthm list-equiv-implies-equal-strsubst-list-3 (implies (list-equiv x x-equiv) (equal (strsubst-list old new x) (strsubst-list old new x-equiv))) :rule-classes (:congruence))

**Theorem: **

(defthm strsubst-list-of-append (equal (strsubst-list old new (append x y)) (append (strsubst-list old new x) (strsubst-list old new y))))

**Theorem: **

(defthm strsubst-list-of-revappend (equal (strsubst-list old new (revappend x y)) (revappend (strsubst-list old new x) (strsubst-list old new y))))

**Theorem: **

(defthm strsubst-list-of-rev (equal (strsubst-list old new (rev x)) (rev (strsubst-list old new x))))