Take $\phi=\forall x_1\,(x_0=x_1)$. The term $x_2$ is <free for substitution> for $x_0$: its variable is not bound by the enclosing quantifier. The term $x_1$ is not <free for substitution> for $x_0$, because insertion under $\forall x_1$ captures that occurrence.

Thus the first substitution gives $\forall x_1(x_2=x_1)$; the second, illegitimate substitution would give $\forall x_1(x_1=x_1)$.

Solution

Past exam of the logic and set theory course of the University of Oxford / 2011 / A / 3 / b / ii / Solution

 Solution (source code)