 Solution

A term $t$ is free for substitution for $x_i$ in $\alpha$ when none of its variables becomes bound at a free occurrence of $x_i$ being replaced. Equivalently, no quantifier surrounding such an occurrence binds a variable of $t$. Bound occurrences of $x_i$ are not replaced. This occurrence-sensitive condition prevents variable capture.

For example take $\alpha (x)=\exists y\neg (x=y)$ and $t=y$. On a two-element domain, $\forall x\exists y\neg (x=y)$ is true. Naive textual substitution produces $\exists y\neg (y=y)$, which is false on every nonempty domain. Thus the corresponding unrestricted A4 implication would be invalid. The problem is that the inserted free $y$ was captured by the existing existential quantifier. Renaming that binder first instead gives the correct instance $\exists z\neg (y=z)$, with $z$ fresh.