Corollary 1.2.10 (Uniqueness of normal form). If a simply typed $\lambda$-term admits a $\beta$-normal form, then it is unique.