Definition 1.2.1 (Simply typed lambda-term). The set ${\mathrm{\Lambda }}_{\mathrm{\Pi }}$ of simply typed $\lambda$-terms is defined by the grammar

$${\mathrm{\Lambda }}_{\mathrm{\Pi }}:=\underset{\text{variables}}{\underbrace{V}}|\underset{\lambda \text{-abstraction}}{\underbrace{\lambda V:\mathrm{\Pi }.{\mathrm{\Lambda }}_{\mathrm{\Pi }}}}|\underset{\lambda \text{-application}}{\underbrace{{\mathrm{\Lambda }}_{\mathrm{\Pi }}{\mathrm{\Lambda }}_{\mathrm{\Pi }}}}.$$

A context is a set of pairs $\{x_1:{\tau }_1,\dots ,x_n:{\tau }_n\}$ where the $x_i$ are (distinct) variables and each ${\tau }_i\in \mathrm{\Pi }$. We write $C$ for the set of all possible contexts. Given a context $\mathrm{\Gamma }\in C$, we also write $\mathrm{\Gamma },x:\tau$ for the context $\mathrm{\Gamma }\cup \{x:\tau \}$ (if $x$ does not appear in $\mathrm{\Gamma }$).

The domain of $\mathrm{\Gamma }$ is the set of variables that occur in it, and the range $|\mathrm{\Gamma }|$ is the set of types that it manifests.