Let $\mathcal T$ be the simply typed lambda calculus whose types are generated from atomic types by $A \to B$, $A \times B$, $A+B$, $\top$, and $\bot$. Terms are generated by variables, lambda abstraction and application, pairing and projections, injections $\operatorname{inl}$ and $\operatorname{inr}$ and case analysis, the unit term $\star$ and unit elimination $\operatorname{let}_{\top}(t;r)$, and empty elimination $\operatorname{abort}_C(t)$. There is no recursion or fixpoint operator. Let $\to_\beta$ be the one-step contextual beta-reduction relation generated by the usual computation rules for these eliminators, and let $\to_\beta^*$ be its reflexive [transitive closure](/theorems/1493). For every well-typed judgment $\Gamma \vdash t:A$, there exist a term $n$ and a finite beta-reduction sequence $t \to_\beta^* n$ such that $n$ is beta-normal, meaning that no term $n'$ satisfies $n \to_\beta n'$.