Proposition 1.2.11 (Uniqueness of types).

• (1)
  If $\mathrm{\Gamma }⊩M:\sigma$ and $\mathrm{\Gamma }⊩M:\tau$, then $\sigma =\tau$.
• (2)
  If $\mathrm{\Gamma }⊩M:\sigma$, $\mathrm{\Gamma }⊩N:\tau$, and $M{\equiv }_{\beta }N$, then $\sigma =\tau$.