left and omit spurious brackets.

-   We identify $\alpha$-equivalent terms, i.e. terms differing only in the names of bound variables are considered identical. We use the symbol $\equiv$ for identity of terms up to $\alpha$-equivalence. We also assume without loss of generality that all bound variables in a term are distinct from the free variables, unless indicated otherwise.[^1]

-   In what follows we use the abbreviations: $$\begin{aligned}
          t_1 : t_2 &\equiv& \mathrm{Is}\, t_1\, t_2 \\
          {\ensuremath{\{ x : \alpha \;|\; \varphi \}}} &\equiv& \mathrm{Subtype}\, \alpha\,
          \lambda x \,.\, \varphi \\
          \alpha \to \beta &\equiv& \mathrm{Fun}\, \alpha\, \beta \\
          \forall x : \alpha \,.\, \varphi &\equiv& \forall\, \alpha\, \lambda x
          \,.\, \varphi \\
          \forall x_1,\ldots,x_n : \alpha \,.\, \varphi &\equiv& \forall x_1 :
          \alpha \,.\, \ldots \forall x_n : \alpha \,.\, \varphi \\
          \varphi \supset \psi &\equiv& \forall x : {\ensuremath{\{ y : {\ensuremath{\mathrm{Prop}}}\;|\; \varphi \}}}
          \,.\, \psi \;\; \mathrm{where\ } x, y \notin FV(\varphi, \psi)
          \\
          \neg \varphi &\equiv& \varphi \supset \bot \\
          \top &\equiv& \bot \supset \bot \\
          \varphi \vee \psi &\equiv& \vee \varphi \psi \\
          \varphi \wedge \psi &\equiv& \neg (\neg \varphi \vee \neg \psi) \\
          \exists x : \alpha \,.\, \varphi &\equiv& \neg \forall x : \alpha
          