\subsection{Canonical forms for $\lc$}


% This fragment has the property of being closed under complementation, 
% \ie if $M$ is a simple term, so is every element of its complement.



\beq
(A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
(A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
P^{\pm} & = & P
\eneq

\begin{metanote}
insert motivating example
\end{metanote}

We then extend it to terms, signatures and contexts as follows:

\beq
(\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
M^{-} & = & M^{+}\\
x^{+} & = & x\\
(M\ N)^{+} & = & (M^{+}\ N^{-})^{1}\\
\skl
(\cdot)^{+} & = & \cdot\\
(\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
(\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+}
\eneq


% \begin{Examplen}
\beq
(y\oftp (a\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} f\ 
x))^{+}  = 
y\oftp (a\TImp a)\RImp a, x\oftp a\vd y(\lamb{f}{a\RImp a} f\ 
x^{1})^{1}
\eneq
% \end{Examplen}


\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1}\bnfalt E\ \ol{x_{n}^{l}}
\end{array} \]

\newcommand{\ctx}{\GG^{+};\cdot;\cdot}

\begin{Ppn}
\label{ppn:embed}
\mbox{}
\ben
\item
If $\GG\vd M\bua A$ then $\ctx\vd M^{-}\bua A^{-}$. 
\item
If $\GG\vd M\da A$ then $\ctx\vd M^{+}\da A^{+}$. 
\enen
\end{Ppn}
\begin{proof}
By simultaneous induction on the proofs of $\GG\vd M\bua A$ and $\GG\vd M\da A$.
\bit
\item Case 
\[\ianc{\GG(x) = A}{\GG\vd x\da A}{atm\_var}\]
Since $x^{+}= x$ and $\GG^{+}(x) = A^{+}$ we conclude by rule 
$cId^{u}$ $\ctx\vd x^{+}\da A^{+}$.
\item
Case 
\[\ibnc{\GG\vd M\da B\Imp A}{\GG\vd N\bua B}{\GG\vd M\ N \da 
A}{atm\_app}\]
By IH on the above two inverted derivations $\ctx\vd M^{+}\da (B\Imp 
A) ^{+}$, \ie $\ctx\vd M^{+}\da B^{-}\RImp 
A ^{+}$ and $\ctx\vd N^{-}\bua B^{-}$. By rule $c\RImp E$ conclude $\ctx\vd 
(M^{+}N^{-})^{1}\da A^{+}$, that is  $\ctx\vd 
((M\ N)^{+} )^{1}\da A^{+}$.
\item Case
\[\ianc{\GG\vd M\da P}{\GG\vd M\bua P}{can\_atm}\]
By HI, $\ctx\vd M^{+}\da P^{+}$ which by  rule $cAt$ yields $\ctx\vd 
M^{+}\bua P^{+}$, \ie by the embedding $\ctx\vd M^{-}\bua P^{-}$.
\item Case 
\[\ianc{\GG,x\oftp A\vd M\bua B}{\GG\vd\lxa M\bua A\Imp B}{canlam}\]
By IH, $x\oftp A^{+},\ctx\vd M^{-}\bua B^{-}$ and  rule $c\RImp E$ yields
$\ctx\vd\lamb{x^{u}}{A^{+}} \bua A^{+}\TImp B^{-}$ and by definition
$\ctx\vd (\lxa M)^{-}\bua (A \Imp B)^{-}$.
\enit
\end{proof}

This embedding yields a sub-language, that we call \emph{simple terms}, which 
corresponds to the embedding of the canonical terms of  the simply-typed 
$\l$-calculus into the strict one, for $n\geq 0$. We thus drop the 
$\pm$ embedding annotations from terms and later from types.

We now prove the crucial exhaustivity lemma

\newcommand{\cu}{(\GG, x\oftp C);\cdot;\cdot}
\newcommand{\cxtr}{\GG;\cdot; x\oftp C}
\newcommand{\cxto}{\GG; x\oftp C;\cdot}


\begin{Ppn}
\label{ppn:embex}\mbox{}
\ben
\item
If $\cu\vd M\da A$ then $\cxtr\vd M\da A$ or $\cxto\vd M\da A$.
\item
If $\cu\vd M\bua A$ then $\cxtr\vd M\bua A$ or $\cxto\vd M\bua A$.
\enen
\end{Ppn}
\begin{proof}
By simultaneous induction on $\cD_{1}::\cu\vd M\da A$ and $\cD_{2}::\cu\vd M\bua A$.
\bit
\item 
$$\cD = \ianc{c\oftp A\in\Sigma}{\cu \prv  c\da A}{cIdc}$$
by the embedding
$$\cE= \ianc{c\oftp A\in\Sigma}{\cxto \prv  c\da A}{cIdc}$$
\item
$$\cD = \ianc{}{(\GG,x\oftp C,y\oftp A);\cdot; \cdot  \prv  y\da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,y\oftp A);x\oftp C; \cdot  \prv  y\da 
A}{cId^{u}}$$
\item No case for $\cD = Id^{1}$.
\item
$$\cD = \ianc{\cu\prv  M\da P}{\cu \prv  M\bua P} {cAt}$$
By inversion $\cu\prv  M\da P$, by HI $\cxtr \prv  M\da P$ or $\cxto \prv  M\da 
P$ and hence $\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$
\item
$$\cD = \ianc{y\oftp A,\cu \prv M\bua B}{\cu\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
By inversion $y\oftp A,\cu \prv M\bua B$ which entails by IH $y\oftp 
A\cxtr \prv M\bua B$ or $y\oftp A\cxto \prv M\bua B$ and finally 
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$
\item
$$\cD = \ibnc{\cu \vd M \da A \RImp B}{\cu \vd N \bua A}{\cu \vd
M\, N^1 \da B}{c\RImp E}$$
By inversion there are derivations $\cD_{1}:: \cu \vd M \da A \RImp 
B$ and $\cD_{2}:: \cu \vd N \bua A$.
There are four disjoint subcases, depending on the `occurrence' status of $x$ 
in $M\ N^{1}$:
\ben
\item $x\in M$. By IH on $\cD_{1}$ and $\cD_{2}$ either $\cxtr\vd M\da 
A\RImp B$ or $\cxto\vd M\da A\RImp B$ and $\cxtr\vd N\bua$ or $\cxto\vd N\bua$;
by rule $c\RImp E$ we get the desired $\cxtr\vd M\ N^{1}\da B$ or $\cxto\vd M\ N^{1}\da B$.
\item $x\in N$. The argument is symmetrical to the above case.
\item $x\in M$ and $x\in N$. Here the IH yields $\cxtr\vd M\da 
A\RImp B$ and $\cxtr\vd N\bua$, hence by weakening the result.
\item $x\not\in M$ and  $x\not\in N$. Here the IH yields $\cxto\vd M\da 
A\RImp B$ an $\cxto\vd N\bua$, hence by weakening   the result.
\enen
\enit
\end{proof}