 Solution

A fresh variable is an arbitrary eigenvariable whose value is not constrained by the undischarged assumptions. For universal introduction, it must not occur free in those assumptions; otherwise a fact about one constrained object could be incorrectly generalized to all objects. For existential elimination, its temporary witness must additionally not occur free in the conclusion or in other undischarged assumptions outside the witness subproof. Choosing a completely unused variable is a sufficient convention. These are the eigenvariable conditions, and concern free occurrences rather than harmless reuse of bound names.