In the simply-typed lambda calculus, do we ever need alpha-conversion in a small-step call-by-value reduction of a term that is closed?

The evaluation rule that uses substitution is:
$(\lambda x.t\_1)~v\_2 \to [x\mapsto v\_2]t\_1$

But if $(\lambda x.t\_1)~v\_2$ is closed, then $v\_2$ is closed and $t\_1$ only has $x$ has a free variable. Since $v\_2$ has no free variables, substitution won't need alpha-conversion. $[x\mapsto v\_2]t\_1$ is also closed because the only free variable, $x$, has been substituted by a close term. So the result of the reduction is also closed.

It's also easy to show that for the other rules, if $t$ is closed and $t \to t'$, then $t'$ is closed.

Therefore, since we only substitute closed terms, $\alpha$-conversion is not needed.

Do you agree?

Edit: Actually, what needs to be shown is that if $t$ is closed and $t \to t'$ then in any immediate reduction $t\_1 \to t\_1'$ used to derive $t \to t'$, $t\_1$ is closed. This is not true when reducing under binders.