A $\l$-context is a set of declarations of the form $x : A$ where $x \in {\cal V}$, $A \in
    {\cal T}$ and where a variable may occur at most once.

2.  A $\l\m$-context is a set of declarations of the form $x : A$ or $\a : \neg B$ where $x \in
    {\cal V}$, $\a \in {\cal W}$, $A,B \in {\cal T}$ and where a variable may occur at most once.

3.  A $\l\m^{\f\et\ou}$-context is a set of declarations of the form $x : A$ or $\a : \neg B$ where $x \in
    {\cal V}$, $\a \in {\cal W}$, $A,B \in {\cal T}'$ and where a variable may occur at most once.

<!-- -->

1.  The simply typed $\l$-calculus (denoted ${\cal S}$) is defined by the following typing rules where $\G$ is a $\l$-context,

    $\F{}{\G , x : A \v x : A} \, ax$ $\F{\G, x: A \v M
    : B} {\G \v \l
    x.M : A \f B} \, \f_i$\
    $\F{\G \v M : A \f B \quad \G \v N : A} {\G \v (M \; N)
    : B }\, \f_e$

2.  The simply typed $\l\m$-calculus (denoted ${\cal S}^{\m}$) is obtained by adding to the previous 