When using a fact like
x = y <=> x + z = y + z as a rewrite rule, it can be desirable to introduce an unused free variable into the result of the rewrite rather than
z, because that keeps open the most options for subsequent substitutions.
Do any proof assistants treat this situation by any means other than automatic renaming or something equivalent? For example, one might require a fresh variable name as an input to the rewriting tactic, or simply leave free variable names as-is? If so, do they have a rationale?
Or is this issue perhaps obviated by the framework or context in which rewriting is done in proof assistants, e.g. working backward from the desired result?