This tactic can be used to force a particular set of names on a goal,
hopefully making the resulting tactic more robust in the face of
underlying implementation changes. Note though that successful use of
this tactic requires that the “new” names in the provided pattern
really be fresh for the goal. If one is really uncertain about what
names might be appearing in a goal, this condition may be difficult to
ensure, particularly as the tactic only looks for one instance of the pattern at a time (but see Q.RENAME_TAC).
This tactic is also available under the alias bossLib.rename1.