Instead, we define the formula $u=v$ (where $u,v$ are terms) to be $\q Y(Y(u) \f Y(v))$ where $Y$ is a unary predicate variable. Such a formula will be called an equation. We denote by $a \approx
    b$, if $a=b$ is a consequence of a set of equations.

-   The formula $F_1 \f (F_2 \f(...\f (F_n \f G)...))$ is also denoted by $F_1,F_2,...,F_n \f G$. For every formula $A$, we denote by $\neg A$ the formula $A \f \perp$. If $\sou{v} = v_1,...,v_n$ is a sequence of variables, we denote by $\q \sou{v} A$ the formula $\q v_1...\q v_n A$.

-   Let $t$ be a $\l$-term, $A$ a type, $\G = x_1 : A_1 ,..., x_n : A_n$ a context, and $E$ a set of equations. We define by means of the following rules the notion “$t$ is of type $A$ in $\G$ with respect to $E$” ; this notion is denoted by $\G\v_{AF2} t:A$ :

<!-- -->

-   \(1) $\G\v_{AF2} x_i:A_i$ $1\leq i\leq n$.

-   \(2) If $\G,x:A \v_{AF2} t:B$, then $\G\v_{AF2} \l xt:A \f B$.

-   \(3) If $\G\v_{AF2} u:A \f B$, and $\G\v_{AF2} v:A$, then $\G\v_{AF2} (u)v:B$.

-   \(4) If $\G\v_{AF2} t:A$, and $x$ is not free in 