If variables can be added to a variable renaming, then the new variables can be added to the ones in the new scope.
Theorem:
(defthm add-var-new-not-error-when-add-var-to-var-renaming (implies (not (reserrp (add-var-to-var-renaming old new ren))) (not (reserrp (add-var new (varset-new ren))))))
Theorem:
(defthm add-vars-new-not-error-when-add-vars-to-var-renaming (implies (not (reserrp (add-vars-to-var-renaming old new ren))) (not (reserrp (add-vars new (varset-new ren))))))