Fix a countably infinite set of variables and a set of base types. Let $\mathsf{Ty}$ be the simple types freely generated from the base types by the function-type constructor $A \to B$. Let $\mathsf{Tm}$ be the pure simply typed lambda terms generated by variables, typed lambda abstractions $\lambda x:A.\,r$, and applications $r\,s$, considered up to alpha-equivalence and equipped with capture-avoiding substitution. Contexts are finite lists of pairwise distinct variable declarations, and typing is given by the standard variable, abstraction, and application rules, with no constants, recursion, or additional typing constructs. Let $\to_\beta$ be the full contextual one-step beta-reduction relation generated by the contraction rule $(\lambda x:A.\,r)\,s \to_\beta r[s/x]$ and closed under reduction in subterms. If $\Gamma \vdash t : A$ is derivable in this calculus, then $t$ is strongly normalizing for $\to_\beta$: there is no infinite sequence \begin{align*} t=t_0 \to_\beta t_1 \to_\beta t_2 \to_\beta \cdots. \end{align*}