Lemma 1.2.5 (Free variables lemma). Assuming that:

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

Then

• (1) If $\mathrm{\Gamma }\subseteq {\mathrm{\Gamma }}^{\prime }$, then ${\mathrm{\Gamma }}^{\prime }⊩M:\sigma$.
• (2) The free variables of $M$ occur in $\mathrm{\Gamma }$.
• (3) There is a context ${\mathrm{\Gamma }}^{\ast }\subseteq \mathrm{\Gamma }$ comprising exactly the free variables in $M$, with ${\mathrm{\Gamma }}^{\ast }⊩M:\sigma$.