Solution
= Solution
\b[False.] Let $\phi$ be $x_i\dot=x_i$ and let $t=x_j$ with $j\ne i$. There is no quantifier that could capture a variable, so $t$ is free for $x_i$ in $\phi$. <Capture-avoiding substitution> gives
$$
\boxed{\phi[t/x_i]=x_j\dot=x_j.}
$$
The number of occurrences of $x_i$ falls from two to zero, contradicting the proposed strict increase. Even <capture-avoiding substitution> of $x_i$ itself would leave the formula unchanged and refute the strict inequality.