Lemma 1.2.6 (Generation Lemma).

• (1)
  For every variable $x$, context $\mathrm{\Gamma }$, and type $\sigma$, if $\mathrm{\Gamma }⊩x:\sigma$, then $x:\sigma \in \mathrm{\Gamma }$;
• (2)
  If $\mathrm{\Gamma }⊩(MN):\sigma$, then there is a type $\tau$ such that $\mathrm{\Gamma }⊩M:\tau \to \sigma$ and $\mathrm{\Gamma }⊩N:\tau$;
• (3)
  If $\mathrm{\Gamma }⊩(\lambda x.M):\sigma$, then there are types $\tau$ and $\rho$ such that $\mathrm{\Gamma },x:\tau ⊩M:\rho$ and $\sigma =(\tau \to \rho )$.