Proposition 1.2.8 (Subject reduction). Assuming that:

• $\mathrm{\Gamma }⊩M:\sigma$

• $M{\to }_{\beta }N$