Lemma 1.2.7 (Substitution Lemma).

• (1)
  If $\mathrm{\Gamma }⊩M:\sigma$ and $\alpha$ is a type variable, then $\mathrm{\Gamma }[\alpha :=\tau ]⊩M:\sigma [\alpha :=\tau ]$;
• (2)
  If $\mathrm{\Gamma },x:\tau ⊩M:\sigma$ and $\mathrm{\Gamma }⊩N:\tau$, then $\mathrm{\Gamma }⊩M[x:=N]:\sigma$.