Theorems about varset-old and varset-new applied to add-var-to-var-renaming and add-vars-to-var-renaming.
These explicate the updated variables in scope when the renaming map is extended.
Theorem:
(defthm varset-old-of-add-var-to-var-renaming (b* ((ren1 (add-var-to-var-renaming old new ren))) (implies (not (reserrp ren1)) (equal (varset-old ren1) (insert (identifier-fix old) (varset-old ren))))))
Theorem:
(defthm varset-old-of-add-vars-to-var-renaming (b* ((ren1 (add-vars-to-var-renaming old new ren))) (implies (and (not (reserrp ren1)) (identifier-listp old)) (equal (varset-old ren1) (set::list-insert old (varset-old ren))))))
Theorem:
(defthm varset-new-of-add-var-to-var-renaming (b* ((ren1 (add-var-to-var-renaming old new ren))) (implies (not (reserrp ren1)) (equal (varset-new ren1) (insert (identifier-fix new) (varset-new ren))))))
Theorem:
(defthm varset-new-of-add-vars-to-var-renaming (b* ((ren1 (add-vars-to-var-renaming old new ren))) (implies (and (not (reserrp ren1)) (identifier-listp new)) (equal (varset-new ren1) (set::list-insert new (varset-new ren))))))