Substitutability in First-Order Logic

Question

Here is a definition for substitutability found in a PDF of logic notes by Eric Pacuit:

I am more concerned with the part of the definition squared in red. My question is: Given $(\forall y) \psi$, does this mean that, since $y$ does not occur free in $(\forall y) \psi$, is $\tau$ substitutable for $y$ in $(\forall y) \psi$?

Answer 1

By definition, the answer is yes, $\tau$ is substitutable for $y$ in $(\forall y)\phi$. This happens because there is nothing that to substitute and, therefore, you not change the original formula.