Closed term and alpha-conversion
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.