Definition 1.2.3 (beta-reduction). The $\beta$-reduction relation is the smallest relation ${\to }_{\beta }$ on ${\mathrm{\Lambda }}_{\mathrm{\Pi }}$ closed under the following rules:

• $(\lambda x:\sigma .P)Q{\to }_{\beta }P[x:=Q]$,

• if $P{\to }_{\beta }{P}^{\prime }$, then for all variables $x$ and types $\sigma \in \mathrm{\Pi }$, we have $\lambda x:\sigma .P{\to }_{\beta }\lambda x:\sigma .P^{\prime }$,

• $P{\to }_{\beta }{P}^{\prime }$ and $z$ as a $\lambda$-term, then $PZ{\to }_{\beta }{P}^{\prime }Z$ and $ZP{\to }_{\beta }Z{P}^{\prime }$.

We also define $\beta$-equivalence ${\equiv }_{\beta }$ as the smallest equivalence relation containing ${\to }_{\beta }$.