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.