Closed term and alpha-conversion 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&#39;$, then $t&#39;$ 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&#39;$ then in any immediate reduction $t_1 \to t_1&#39;$ used to derive $t \to t&#39;$, $t_1$ is closed. This is not true when reducing under binders.
This is true as long as you're only reducing towards a weak head normal form. But if you want to go further, you start reducing under lambdas. If you're looking at the pure lambda-calculus (typed or not), you must be reducing under lambdas if you're reducing closed terms. And when you're reducing under lambdas, you're no longer operating on closed terms.

Here's an example that starts with a closed lambda-term where all binding sites use unique names, proceeds to a term with repeated but non-capturing binders, then reaches a term with capture, which requires alpha-conversion to proceed. The initial term is not simply-typed, but you can remedy this by changing it to $(\lambda w. (\lambda z. w z z) (\lambda x. \lambda y. x y))$ which is simply-typed and shows the same binding-related issues.

$$
\begin{array}{rl}
(\lambda \underline{z}. \underline{z} \underline{z}) \underline{(\lambda x. \lambda y. x y)}
\quad \to &amp;
(\lambda \underline{x}. \lambda \color{blue}{y}. \underline{x} \color{blue}{y}) \underline{(\lambda x. \lambda \color{red}{y}. x \color{red}{y})}
\\ \to &amp;
(\lambda \color{blue}{y}. (\lambda \underline{x}. \lambda \color{red}{y}. \underline{x} \color{red}{y}) \underline{\color{blue}{y}})
\\ \to &amp;
(\lambda \color{blue}{y}. \lambda \color{red}{y}. \color{blue}{y} \color{red}{y})
\end{array}
$$

That last step requires alpha-conversion, to make the blue $y$ and the red $y$ distinct.

Your proof sketch is correct as long as you apply the beta rule in a context that does not bind any variable. If you extend the proof to the lambda context case, it fails when $x$ is in the context.