\chapter{A Strict $\l$-Calculus}
\label{ch:strict}

In this Chapter we introduce a strict $\l$-calculus and develop its
basic properties, culminating in the existence of canonical
forms~\ref{sec:canonthm}.  Chapter \ref{ch:relcomp} will introduce a
restriction of the language for which complementation is possible.


\section{Strict Types}
\label{sec:strict}

As we have seen in the preceding Chapter, the complement of a
partially applied pattern in the simply-typed $\lambda$-calculus
cannot be expressed in a finitary manner within the same calculus.  We
thus generalize our language to include \emph{strict functions} of
type $A \RImp B$ (which are guaranteed to depend on their argument)
and \emph{invariant functions} of type $A \ZImp B$ (which are
guaranteed \textbf{not} to depend on their argument).  Of course, any
concretely given function either will or will not depend on its
argument, but in the presence of existential variables we still need
the ability to remain uncommitted.  Therefore our calculus also
contains the full function space $A \UImp B$. A similar calculus has
been independently investigated in \cite{Wright91,Baker94}: for a comparison
see Section \ref{sec:relstrict}.


\[ \begin{array}{rrcl}
 \mbox{\textit{Labels}} & k & \bnfas & 1 \bnfalt 0 \bnfalt u \\
 \mbox{\textit{Types}} & A & \bnfas & a \bnfalt A_1 \GImp{k} A_2 \\
 \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam
 x^k\oftp A\ldot M \bnfalt (M_1 \ M_2)^k \\ \mbox{\textit{Contexts}} &
 \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
 \end{array} \]

Note that there are three different forms of abstractions and
applications, where the latter are distinguished by different labels
on the argument.  It is not really necessary to distinguish three
forms of application syntactically, since the type of function
determines the status of the application, but it is convenient for our
purposes.  If a label is $u$ it is called \emph{undetermined},
otherwise it is \emph{determined} and denoted with the metavariable
$d$.


We use a formulation of the typing judgment with three zones,
containing the unrestricted, irrelevant and strict hypotheses, denoted
by $\Gamma$, $\Omega$, and $\Delta$, respectively.  \[ \Gamma; \Omega;
\Delta \vd M \hastype A \] We implicitly assume a fixed signature
$\Sigma$ which would otherwise clutter the presentation.  Recall that
$\Gamma_1,\Gamma_2$ is a union of two contexts which do not declare
any common variables.  Recall also that we consider contexts as sets,
that is, exchange is left implicit.

\begin{figure}

\[ \begin{array}{c}
 \ianc{c\oftp A \in \Sigma}{\Gamma; \Omega; \cdot \vd c \hastype
 A}{Con} \\[1em]

 \ianc{}{(\Gamma, x\oftp A); \Omega; \cdot \vd x \hastype A}{Id^u}
 \hspace{2em} \mbox{\textit{no $Id^0$ rule}} \hspace{2em}
 \ianc{}{\Gamma; \Omega; x\oftp A \vd x \hastype A}{Id^1} \\[1em]

 \ianc{(\Gamma, x\oftp A); \Omega; \Delta \vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^u \oftp A\ldot M \hastype A \GImp{u}
B}{\GImp{u}I} \\[1em]

 \ianc{\Gamma; (\Omega, x\oftp A); \Delta \vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^0 \oftp A\ldot M \hastype A \GImp{0}
B}{\GImp{0}I} \\[1em]

 \ianc{\Gamma; \Omega; (\Delta, x\oftp A)\vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^1 \oftp A\ldot M \hastype A \GImp{1}
B}{\GImp{1}I} \\[1em]

 \ibnc{\Gamma; \Omega; \Delta \vd M \hastype A \UImp B}{(\Gamma,
\Delta); \Omega; \cdot \vd N \hastype A}{\Gamma; \Omega; \Delta \vd M\
N^u \hastype B}{\GImp{u}E} \\[1em]

 \ibnc{\Gamma; \Omega; \Delta \vd M \hastype A \ZImp B}{(\Gamma,
\Omega,\Delta); \cdot; \cdot \vd N \hastype A}{\Gamma; \Omega; \Delta
\vd M\ N^0 \hastype B}{\GImp{0}E} \\[1em]

\ibnc{(\Gamma, \Delta_N); \Omega; \Delta_M \vd M \hastype A \RImp
B}{(\Gamma, \Delta_M); \Omega; \Delta_N \vd N \hastype A}{\Gamma;
\Omega; (\Delta_M, \Delta_N) \vd M\ N^1 \hastype B}{\GImp{1}E}

 \end{array} \]
\caption{Typing rules for $\lc$}
\label{fig:typrules}
\end{figure}

Our system is biased towards a bottom-up reading of the rules in that
variables never disappear, \ie they are always propagated from the
conclusion to the premises, although their status might be changed.

Let us go through the typing rules in detail.  The requirement for the
strict context $\Delta$ to be empty in the $Id^u$ and $Id^1$ rules
expresses that strict variables must be used, while undetermined
variables in $\Gamma$ or irrelevant variables in $\Omega$ can be
ignored.  Note that there is no rule for irrelevant variables, which
expresses that they cannot be used.

The introduction rules for undetermined, invariant, and strict
functions simply add a variable to the appropriate context and check
the body of the function.

The difficult rules are the three elimination rules.  First, the
undetermined context $\Gamma$ is always propagated to both premises.
This reflects that we place no restriction on the use of these
variables.

Next we consider the strict context $\Delta$.  Recall that this
contains the variables which should occur strictly in a term.  An
undetermined function $M\hastype A \GImp{u} B$ may or may not use its
argument.  An occurrence of a variable in the argument to such a
function can therefore not be guaranteed to be used.  Hence we must
require in the rule $\GImp{u}E$ for an application $M\ N^u$ that all
variables in $\Delta$ occur strictly in $M$.  This ensures at least
one strict occurrence in $M$ and no further restrictions on
occurrences of strict variables in the argument are necessary.  This
is reflected in the rule by adding $\Delta$ to the undetermined
context while checking the argument $N$.  The treatment of the strict
variables in the vacuous application $M\ N^0$ is similar.

In the case of a strict application $M\ N^1$ each strict variable
should occur strictly in either $M$ or $N$.  We therefore split the
context into $\Delta_M$ and $\Delta_N$ guaranteeing that each variable
has at least one strict occurrence in $M$ or $N$, respectively.
However, strict variables can occur more than once, so variables from
$\Delta_N$ can be used freely in $M$, and variables from $\Delta_M$
can occur freely in $N$.  As before, we reflect this by adding these
variables to the undetermined context.

Finally we consider the irrelevant context $\Omega$.  Variables
declared in $\Omega$ cannot be used \emph{except} in the argument to
an irrelevant function (which is guaranteed to ignore its argument).
We therefore add the irrelevant context $\Omega$ to the undetermined
context when checking the argument of a vacuous application $M\ N^0$.

%sample derivation

\newcommand{\jj}{\justifies}
% \begin{Examplen}
\begin{figure}
\newcommand{\aaa}{y \oftp A; \cdot; x  \oftp A \RImp A\RImp B \prv x
\hastype A \RImp A\RImp B}
\newcommand{\bbb}{x\oftp A \RImp A\RImp B;\cdot ; y  \oftp A\prv
 y\hastype A }
\newcommand{\ccc}{\cdot;\cdot ;( x  \oftp A \RImp A\RImp B , y  \oftp
  A)\prv x y^1 \hastype A\RImp B}
\newcommand{\ddd}{ (x \oftp A \RImp A\RImp B, y  \oftp A); \cdot
  ;\cdot\prv y\hastype A}
\newcommand{\eee}{ \cdot;\cdot; (x  \oftp A \RImp A\RImp B ,y\oftp
  A)\prv (x y^1)  y^1 \hastype B}
\begin{small}
\prooftree
\[
\[ \mbox{} \jj \aaa\using Id^1\]
\quad 
\[ \mbox{} \jj \bbb\using Id^1\]
\jj \ccc\using \RImp E\]
\quad
\[ \mbox{} \jj \ddd\using Id^u\]
\jj
\eee
\using \RImp E
\endprooftree
\end{small}
\caption{First derivation of $\cdot;\cdot; (x  \oftp A \RImp A\RImp B ,y\oftp A)\prv (x y^1)  y^1\hastype B$}
\label{fig:strictex}
\end{figure}

We now illustrate how the strict application rule
non-deterministically splits contexts. Consider the typing problem
$\cdot;\cdot; (x \oftp A \RImp A\RImp B ,y\oftp A)\prv (x y^1)
y^1\hastype B$.  There are four ways to split the strict context:

\[\begin{array}{ll}
\D_{M} = x \oftp A \RImp A\RImp B ,y\oftp A & \D_{N}=\cdot\\ \D_{M} =
x \oftp A \RImp A\RImp B & \D_{N} = y\oftp A\\ \D_{M} = y\oftp A &
\D_{N}= x \oftp A \RImp A\RImp B\\ \D_{M} =\cdot & \D_{N}=x \oftp A
\RImp A\RImp B ,y\oftp A
\end{array}\]
Only the first two yield a valid derivation (depicted in
Figure~\ref{fig:strictex} and Figure~\ref{fig:strictex2}), as $x$ needs to
be strict in the leftmost branch.


\begin{figure}
\newcommand{\aaa}{y \oftp A; \cdot; x  \oftp A \RImp A\RImp B \prv x
\hastype A \RImp A\RImp B}
\newcommand{\bbb}{(x\oftp A \RImp A\RImp B, y  \oftp A);\cdot;\cdot\prv
 y\hastype A }
\newcommand{\ccc}{y\oftp A;\cdot ; x  \oftp A \RImp A\RImp B \prv x y^1 \hastype A\RImp B}
\newcommand{\ddd}{ x \oftp A \RImp A\RImp B;\cdot; y  \oftp A\prv y\hastype A}
\newcommand{\eee}{ \cdot;\cdot; (x  \oftp A \RImp A\RImp B ,y\oftp
  A)\prv (x y^1)  y^1 \hastype B}
\begin{small}
\prooftree
\[
\[ \mbox{} \jj \aaa\using Id^1\]
\quad 
\[ \mbox{} \jj \bbb\using Id^u\]
\jj \ccc\using \RImp E\]
\quad
\[ \mbox{} \jj \ddd\using Id^1\]
\jj
\eee\using \RImp E
\endprooftree
\end{small}
\caption{Second derivation of  $\cdot;\cdot; (x  \oftp A \RImp A\RImp B ,y\oftp A)\prv (x y^1)  y^1\hastype B$}
\label{fig:strictex2}
\end{figure}


Our strict $\lambda$-calculus satisfies the expected properties,
culminating in the existence of canonical forms which is critical for
the intended applications.  We begin with the following:

\begin{Remark}[Inversion]
\label{rmk:invert}
All rules in $\lc$ are invertible.
\end{Remark}
 We will often use inversion principles tacitly
in proofs by structural induction on the typing derivation.


Note that, although typing derivation may not, typing is unique.

\begin{Theorem}[Uniqueness of Typing]
\label{thm:uniqueT}
If $\god\vd M\hastype A$ and $\GG';\O';\D\vd M\hastype A'$, then
$A\equiv A'$.
\end{Theorem}
\begin{proof}
By induction on the structure of the given derivations, exploiting
`functionality' of signatures and contexts.
\end{proof}


We start addressing the structural properties of the context(s).
Exchange is directly built into the formulation and will not be
repeated.


 \begin{Theorem}[Weakening] \mbox{}
 \label{thm:weak}
 \begin{enumerate}
  \item (Weakening$^{u}$) If $\Gamma; \Omega; \Delta\vd M \hastype A$,
then $(\Gamma, x\oftp C); \Omega; \Delta\vd M \hastype A$.
  \item (Weakening$^{0}$) If $\Gamma; \Omega; \Delta\vd M \hastype A$,
then $\Gamma ; (\Omega, x\oftp C); \Delta\vd M \hastype A$.
  \end{enumerate}
  \end{Theorem}
 
\begin{proof}
By induction on the structure of the given derivation.
\end{proof}
 
 
The following properties allow us to lose track of strict and vacuous occurrences, if we
are so inclined. We use the phrase `by sub-derivation' to localize the
immediate sub-derivation(s) of a given one; `by rule' means in this
Chapter by application of the correct (and unique) typing rule, when
not explicitly mentioned.

\newcommand{\gofd}{\GG;(\Omega,x\oftp C);\Delta}
\newcommand{\gfod}{(\GG,x\oftp C);\Omega;\Delta}


\begin{Theorem}
\label{thm:0loosex}
If $\gofd\vd M \hastype A$, then $\gfod\vd M \hastype A$.
\end{Theorem}

\begin{proof}
By induction on the structure of $\cD ::\gofd\vd M\hastype A$ .  \bit

\itc $$\cD = \ianc{c\oftp A\in\Sigma}{\Gamma; (\Omega,x\oftp C);\cdot
\prv c\hastype A}{Idc}$$ Then
$$\cE= \ianc{c\oftp A\in\Sigma}{(\GG,\xoc);\Omega;\cdot \prv c\hastype
A}{Idc}$$
%\item

\itc $$\cD = \ianc{}{(\Gamma,y\oftp A); (\Omega,\xoc);\cdot\vd
y\hastype A}{Id^{u}}$$ Then
$$\cE = \ianc{}{(\Gamma,y\oftp A,\xoc);\Omega;\cdot\vd y\hastype
A}{Id^{u}}$$

\itc $$\cD = \ianc{}{\Gamma;(\Omega,\xoc);y\oftp A\prv y\hastype
A}{Id^{1}}$$ Then
$$\cE=\ianc{}{(\Gamma,\xoc);\Omega;y\oftp A\prv y\hastype A}{Id^{1}}$$

\itc $$\cD = \ianc{\arv{\cD'}{\GG;(\Omega,\xoc,y\oftp A);\Delta\prv M\hastype B}}
{\gofd\prv(\lamb{y^0}{A} M) \hastype A\ZImp B} {\ZImp I}$$ 
\btab
$\GG;(\Omega,\xoc,y\oftp A);\Delta\prv M\hastype B$ \` By
sub-derivation\\ 
$(\GG,\xoc);(\Omega,y\oftp A);\Delta\prv M\hastype B$
\` By IH on $\cD'$\\
 $\gfod\prv(\lamb{y^0}{A} M) \hastype A\ZImp B$\` By rule
$\ZImp I$
 \etab

\itc $\cD$ ends in $\TImp I$ or $\RImp I$: the claim follows from an
immediate appeal to the inductive hypothesis, as in the above case.

\itc $$\cD = \ibnc{\arv{\cD_1}{\gofd \vd M \hastype A \TImp B}}
{\arv{\cD_2}{(\GG,\Delta);(\Omega,\xoc);\cdot \vd N \hastype A}}{\gofd \vd M\ N^u
\hastype B}{\TImp E}$$ 
\btab $\cD_1::\gofd \vd M \hastype A \TImp B$\bs
 $\gfod\vd M \hastype A \TImp B$ \bi on $\cD_1$\\ 
$\cD_2::(\GG,\Delta);(\Omega,\xoc);\cdot \vd N \hastype A$\bs
$(\GG,\D,\xoc);\Omega;\cdot\vd N \hastype A$\bi on $\cD_2$\\ 
$\gfod\vd M \ N^{u}\hastype B$\br $\TImp E$ \etab

\itc $$\cD = \ibnc{\arv{\cD_1}{\gofd \vd M \hastype A \ZImp B}}
{\arv{\cD_2}{(\GG,\Omega,\Delta,\xoc);\cdot;\cdot \vd N \hastype A}}{\gofd \vd M\
N^0\hastype B}{\ZImp E}$$ 
\btab 
$\gofd \vd M \hastype A \ZImp B$\bs 
$\gfod\vd M \hastype A \ZImp B$ \bi on $\cD_1$\\
$(\GG,\Omega,\D,\xoc);\cdot;\cdot\vd N \hastype A$\bs 
$\gfod\vd M \ N^{0}\hastype B$\br $\ZImp E$ \etab

\itc $$\cD =
\ibnc{\arv{\cD_1}{(\GG,\Delta_{N});(\Omega,\xoc);\Delta_{M} \vd M \hastype A
\RImp B}}{\arv{\cD_2}{(\GG,\Delta_M);(\Omega,\xoc);\Delta_{N}\vd N \hastype
A}}{\GG;(\Omega,\xoc);(\Delta_{N},\Delta_{M}) \vd M\ N^1 \hastype
B}{\RImp E}$$
 \btab
 $(\GG,\Delta_{N});(\Omega,\xoc);\Delta_{M}
\vd M \hastype A \RImp B$\bs 
$(\GG,\xoc,\Delta_{N});\Omega;\Delta_{M}
\vd M \hastype A \RImp B$\bi on $\cD_1$\\
$(\GG,\Delta_M);(\Omega,\xoc);\Delta_{N}\vd N \hastype A$\bs
$(\GG,\xoc,\Delta_M);\Omega;\Delta_{N}\vd N \hastype A$\bi on $\cD_2$\\
 $(\GG,\xoc);\Omega;(\Delta_{N},\Delta_{M})\vd M \
N^{1}\hastype B$\br $\RImp E$ 
\etab \enit\end{proof}

\begin{Corollary}[Loosening$^{0}$]
\label{thm:0loose}
If $\Gamma; (\Omega,\Phi); \Delta\vd M \hastype A$, then $(\Gamma,
\Phi); \Omega; \Delta\vd M \hastype A$.
\end{Corollary}
\begin{proof}
By repeated application of Theorem \ref{thm:0loosex}.
\end{proof}

\newcommand{\godx}{\Gamma; \Omega; (\Delta,x\oftp C)}
\newcommand{\gdo}{(\GG,x\oftp C);\Omega;\Delta}

\begin{Theorem}
\label{thm:1loosex}

If $\Gamma; \Omega; (\Delta,x\oftp C)\vd M \hastype A$, then $\gdo\vd
M \hastype A$.
\end{Theorem}

\begin{proof}
By induction on the structure of $\cD ::\godx\vd M\hastype A$.  \bit
\itc $\cD$ ends in $Con,Id^{u}$: vacuously true.  \itc $$\cD =
\ianc{}{\Gamma;\Omega;x\oftp A\prv x\hastype A}{Id^{1}}$$ Then
$$\cE=\ianc{}{(\Gamma,x\oftp A);\Omega;\cdot\prv x\hastype
A}{Id^{u}}$$

\itc $$\cD = \ianc{\GG;\Omega;(\Delta,x\oftp C,y\oftp A)\prv M\hastype
B} {\godx\prv(\lamb{y^1}{A} M) \hastype A\RImp B} {\RImp I}$$ \btab
$\GG;\Omega;(\Delta,x\oftp C,y\oftp A)\prv M\hastype B$ \` By
sub-derivation \\ $(\GG,x\oftp C,);\Omega;(\D,y\oftp A) \prv M\hastype
B$ \` By IH\\ $\gdo\prv(\lamb{y^1}{A} M) \hastype A\RImp B$ \` By rule
\etab

\itc $\cD$ ends in $\TImp I$ or $\ZImp I$: the thesis follow from an
immediate appeal to the inductive hypothesis as in the above case.

\itc $$\cD = \ibnc{\godx \vd M \hastype A \TImp B}{(\GG,\Delta,x\oftp
C);\Omega;\cdot \vd N \hastype A}{\godx \vd M\ N^u\hastype B}{\TImp
E}$$ \btab $\godx \vd M \hastype A \TImp B$ \` By sub-derivation \\
$\gdo\vd M \hastype A \TImp B$ \` By IH\\ $(\GG,\Delta,x\oftp
C),\Omega;\cdot\vd N \hastype A$ \` By sub-derivation \\ $\gdo\vd M \
N^{u}\hastype B$ \` By rule \etab

\itc $$\cD = \ibnc{\godx \vd M \hastype A \ZImp
B}{(\GG,\Omega,\Delta,x\oftp C);\cdot;\cdot \vd N \hastype A}{\godx
\vd M\ N^0\hastype B}{\ZImp E}$$ \btab $\godx \vd M \hastype A \ZImp
B$ \` By sub-derivation \\ $\gdo\vd M \hastype A \ZImp B$ \` By IH \\
$(\GG,\Omega,\Delta,x\oftp C);\cdot;\cdot \vd N \hastype A$ \` By
sub-derivation\\ $\gdo\vd M \ N^{0}\hastype B$ \` By rule \etab \itc
$\cD$ ends in $\RImp$. There are two sub-cases: \bit
\item[ $x\in\D_{M}$] $\cD$ =
$$ \ibnc{(\GG,\Delta_{N});\Omega;(\D'_M,x\oftp C) \vd M \hastype A
\RImp B} {(\GG,\D'_M,x\oftp C);\Omega;\Delta_{N} \vd N \hastype A}
{\GG;\Omega;(\D'_M,x\oftp C,\Delta_{N})\vd M\ N^1 \hastype B}{\RImp
E}$$ \btab $(\GG,\Delta_{N});\Omega;(\D'_M,x\oftp C) \vd M \hastype A
\RImp B$ \` By sub-derivation\\ $(\GG,\Delta_{N},x\oftp C);\Omega;\D'_M
\vd M \hastype A \RImp B$ \` By IH\\ $(\GG,\D'_M,x\oftp
C);\Omega;\Delta_{N} \vd N \hastype A$ \` By sub-derivation \\
$(\GG,x\oftp C);\Omega;(\Delta_{N},\D'_M)\vd M \ N^{1}\hastype B$\br
\etab
\item[ $x\in\D_N$] Symmetrical to the above.  \enit\enit
\end{proof}

\begin{Corollary}[Loosening$^{1}$]
\label{thm:1loose}
If $\Gamma; \Omega; \Delta\vd M \hastype A$, then $(\GG,\D);\O;\cdot\vd
M \hastype A$.
\end{Corollary}
\begin{proof}
By repeated application of Theorem \ref{thm:1loosex}.
\end{proof}


\begin{Theorem}[Substitution Properties] \mbox{}
\label{thm:substitution}
\begin{enumerate}
\item (Substitution$^u$) If $(\Gamma, x\oftp A);\Omega;\Delta\vd M
\hastype C$ and $(\Gamma,\D); \Omega;\cdot \vd N \hastype A$, then
$\Gamma;\Omega;\Delta \vd [N/x]M \hastype C$.
 \item (Substitution$^0$) If $\Gamma;(\Omega,x\oftp A);\Delta \vd M
\hastype C$ and $(\Gamma, \Delta,\Omega) ;\cdot;\cdot \vd N \hastype
A$, then $\Gamma;\Omega;\Delta \vd [N/x]M \hastype C$.  \item
(Substitution$^1$) If $(\Gamma,\Delta_N);\Omega; (\Delta_M, x\oftp A
)\vd M \hastype C$ and $(\Gamma,\Delta_M);\Omega;\Delta_N \vd N
\hastype A$, then \\
$\Gamma; \Omega;( \Delta_M, \Delta_N) \vd [N/x]M
\hastype C$.
\end{enumerate}
\end{Theorem}

\begin{proof}
The proof is by mutual induction on the height of the derivation $\cD$
of $M\hastype C$.  We show the crucial cases.  
\ben
\item \fbox{Substitution$^u$}\mbox{} 
\bit 
\itc
$$\cD = \ianc{c\oftp C\in\Sigma}{ (\Gamma, x\oftp A);\Omega;\cdot\vd c
\hastype C}{Con}$$ As $[N/x] c= c$, then
$$\cF = \ianc{c\oftp C\in\Sigma}{\GG;\Omega;\cdot\vd c \hastype
C}{Con}$$ 
\itc
$$\cD = \ianc{}{ (\Gamma', x\oftp A,y\oftp C);\Omega;\cdot\vd y
\hastype C} {Id^u}$$ As $[N/x] y= y$, then
$$\cF = \ianc{}{(\GG',y\oftp C);\Omega;\cdot\vd y \hastype C}{Id^u}$$
\itc
$$\cD = \ianc{}{(\Gamma, x\oftp A);\Omega;\cdot\vd x \hastype
C}{Id^u}$$ As $[N/x] x= N$ and $C=A$, then
$\cF=\cE::\GG;\Omega;\cdot\vd N \hastype C$
% $$\cF = \ianc{}{\GG;\Omega;\cdot\vd N \hastype C}{Id^u}$$
\itc
$$\cD = \ianc{}{ (\Gamma, x\oftp A);\Omega;y\oftp C\vd y \hastype
C}{Id^1}$$ As $[N/x] y= y$, then
$$\cF = \ianc{}{\GG;\Omega;y\oftp C\vd y \hastype C}{Id^1}$$ 
\itc
$$\cD=\ianc{(\GG,\xoa,y\oftp B);\O;\D\vd M\hastype
C}{(\GG,\xoa);\O;\D\vd \lamb{y^u}{B} M\hastype B\TImp C}{\TImp I}$$
\btab $(\GG,\xoa,y\oftp B);\O;\D\vd M\hastype C$\bs
$\GG;\Omega;\cdot\vd N \hastype C$\bh 
$(\GG,y\oftp B);\Omega;\cdot\vd N
\hastype C$\` By Weakening$^u$\\
$(\GG,y\oftp B);\Omega;\D\vd [N/x]M\hastype C$\bi \\
$\GG;\O;\D\vd  (\lamb{y^u}{B}[N/x]M)\hastype A\TImp B$\br\\
$\GG;\O;\D\vd [N/x] (\lamb{y^u}{B}M)\hastype A\TImp B$\bsu
 \etab 
\itc $\cD$ ends with $ \ZImp I,  \RImp I$: similarly.
\itc
$$ \cD= \ibnc{\arv{\cD_1}{ (\GG, x\oftp A); \Omega; \Delta \vd P
\hastype B \UImp C}} {\arv{\cD_{2}}{ (\Gamma, \Delta, x\oftp A);
\Omega; \cdot \vd Q \hastype B}}{(\GG, x\oftp A); \Omega; \Delta \vd
P\ Q^u \hastype C}{\GImp{u}E}$$ 
\btab $ (\GG, x\oftp A); \Omega;
\Delta \vd P \hastype B \UImp C$ \` By sub-derivation \\
 $\cE ::
(\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$\god\vd[N/x]P\hastype B \UImp C$ \` By IH on $\cD_{1}$ and $\cE$\\ 
$(\GG, x\oftp A,\Delta); \Omega;\cdot \vd Q\hastype B$ \` By
sub-derivation\\
%$(\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$(\GG,\D);\O;\cdot\vd[N/x]Q\hastype B$ \` By IH on $\cD_2$ and $\cE$\\
$\GG; \Omega; \Delta\vd ([N/x]P) ([N/x] Q)^u \hastype C$ \` By rule \\
$\GG; \Omega; \Delta\vd [N/x] (P\ Q^u) \hastype C$ \` By substitution. 
 \etab
\itc
$$\cD= \ibnc{\arv {\cD_1}{ (\GG, x\oftp A); \Omega; \Delta \vd P
\hastype B \ZImp C}} {\arv{\cD_2}{ (\Gamma, \Delta, \Omega,x\oftp A);
\cdot; \cdot \vd Q \hastype B}}{(\GG, x\oftp A); \Omega; \Delta\vd P\
Q^0 \hastype C}{\GImp{0}E}$$ 
\btab
$ (\GG, x\oftp A); \Omega; \Delta \vd P \hastype B \ZImp C$ \` By sub-derivation\\
$\cE :: (\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$\god\vd[N/x]P\hastype  B \ZImp C$ \` By IH on $\cD_{1}$ and $\cE$\\
$ (\GG, x\oftp A,\O,\Delta); \cdot;\cdot \vd Q \hastype B$ \` By sub-derivation\\
%$(\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$\cE'::(\GG,\D,\O);\cdot;\cdot\vd N\hastype A$ \` By Loosening$^{0}$
$\Omega$ in $ \cE$ \\
$(\GG,\D,\O);\cdot;\cdot\vd[N/x]Q\hastype  B$ \` By IH on $\cD_2$ and $\cE'$\\
$\GG; \Omega; \Delta\vd [N/x] (P\ Q)^0 \hastype C$ \` By rule
\etab
\itc
$\cD= $
$$ \ibnc{\arv {\cD_1}{ (\GG, x\oftp A,\D_{Q}); \Omega; 
\Delta_{P} \vd P \hastype B \RImp C}} {\arv{\cD_2}{ 
(\Gamma,x\oftp A,\D_{P});\Omega;\D_{Q} \vd Q \hastype B}} 
{(\GG, x\oftp A); \Omega; (\Delta_{P},\D_{Q})
\vd P\ Q^1 \hastype C}{\GImp{1}E}$$
\btab
$(\GG, x\oftp A,\D_{Q}); \Omega; \Delta_{P} \vd P \hastype 
B \RImp C$ \` By sub-derivation\\
$\cE :: (\GG,\D_{P},\D_{Q});\O;\cdot\vd N\hastype A$
 \` By hypothesis\\
$(\GG,\D_{Q});\O;\D_{P}\vd[N/x]P\hastype  B \RImp C$
 \` By IH on $\cD_{1}$ and $\cE$\\
$  (\GG, x\oftp A,\D_{P}); \Omega; 
\Delta_{Q} \vd Q \hastype B $ \` By sub-derivation\\
% $\cE' :: (\GG,\D_{P},\D_{Q});\O;\cdot\vd N\hastype A$
% \` By hypothesis\\
$(\GG,\D_{P});\O;\D_{Q}\vd[N/x]Q\hastype  B$
 \` By IH on $\cD_{2}$ and $\cE$\\
$\GG; \Omega; (\Delta_{P},\D_{Q})\vd [N/x] (P\ Q)^1 \hastype C$
 \` By rule
\etab
\enit
\item \fbox{Substitution$^0$} 
Similar to the above.
\item \fbox{Substitution$^1$} \mbox{} 

\bit
\itc $\cD$ ends in   $Con,Id^{u}$: vacuously true.
\itc  
$$\cD = \ianc{}{(\GG,\D_N);\O;x\oftp A\vd x\hastype A}{Id^{1}}$$
and $[N/x]x  = N$;  then $\D_M=\cdot$, $\cF=\cE::\GG;\O;\D_{N}\vd  N$.
% $${\cal F} = \ianc{}{\GG;\O;\D_{N}\vd  N}{Id^{1}}$$
\itc
 $$\cD= \ianc{\arv{\cD_1}{(\GG,\D_N);(\O,y\oftp B);(\D_{M},x\oftp 
A)\vd Q\hastype C}}{(\GG,\D_N);\O;(\D_{M},x\oftp A)\vd \lamb 
{y^{0}} {B} Q\hastype B\ZImp C}{\ZImp I}$$
\btab
$\cD_1::(\GG,\D_N);(\O,y\oftp B);(\D_M,x\oftp 
A)\vd Q\hastype C$\` By sub-derivation\\
 $\cE::(\GG,\D_M);\O;\D_{N}\vd N\hastype A$ 
\` By hypothesis\\
$\cE'::(\GG,\D_M);(\O,y\oftp B);\D_{N}\vd N\hastype A$
\`  By Weakening$^{0}$ on $\cE$\\
$\GG;(\O,y\oftp B);\dmn\vd [N/x] Q\hastype C$
\` By IH on $\cD_1$ and $\cE'$\\
 $\GG;\O;\dmn\vd \lamb{y^{0}}{B} [N/x]Q\hastype B\ZImp C$
\` By rule\\
 $\GG;\O;\dmn\vd [N/x] (\lamb{y^{0}}{B} Q)\hastype B\ZImp C$\` By substitution.
\etab
\itc $\cD$ ends with $\TImp I$.  Proceed similarly  using 
Weakening$^{u}$.  
\itc $\cD$ ends with $\RImp I$. It  follows by an immediate appeal to the IH.
\itc
$$\cD=\ibnc{(\GG,\D_N);\O;(\D_M,x\oftp A)\vd P\hastype 
B\TImp C}
{(\GG,\D_M,x\oftp A,\D_N);\O;\cdot\vd Q\hastype B}
{(\GG,\D_N);\O;(\D_M,x\oftp A)\vd P\ Q^{u}\hastype C}{\TImp E}$$
\btab
$ \cD_1::(\GG,\D_N);\O;(\D_M,x\oftp A)\vd P \hastype B \UImp C$ \` By sub-derivation\\
$\cE :: (\GG,\D_M);\O;\D_N\vd N\hastype A$ \` By hypothesis\\
$\GG;\O;(\D_M,\D_{N})\vd[N/x]P\hastype  B \UImp C$ \` By IH on $\cD_{1}$ and $\cE$\\
$\cD_2::(\GG,\D_M,x\oftp A,\D_N);\O;\cdot\vd Q\hastype  B$ \` By sub-derivation\\
%$(\GG,\D_M);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$(\GG,\D_M,\D_{N});\O;\cdot\vd[N/x]Q\hastype  B$ \` By IH on $\cD_2$ and $\cE$\\
$\GG; \Omega; (\Delta_M,\D_{N})\vd [N/x] (P\ Q)^u \hastype C$ \` By rule
\etab
\itc
$\cD$ ends in $\ZImp E$: similar.
\itc $\cD$ ends in $\RImp E$: there are two sub-cases\fixed, where $\D_M=\D_P,\D_Q$:
\bit
\item[\textbf{$x\in \D_{P}$}]\mbox{}
$\cD=$
%\begin{small}
$$
 \ibnc{\arv {\cD_1}{ (\GG,\D_{N},\D_{Q}); \Omega; 
(\Delta'_{P}, x\oftp A) \vd P \hastype B \RImp C}} {\arv{\cD_2}{ 
(\Gamma,\D_{N},x\oftp A,\D'_{P});\Omega;\D_{Q} \vd Q \hastype B} }
{(\GG,\D_N); \Omega; (\Delta'_{P}, x\oftp A,\D_{Q})\vd P\ Q^1 \hastype
  C}{\GImp{1}E}$$
%\end{small}
\btab
$\cD_1::(\GG,\D_{N},\D_{Q}); \Omega; (\Delta'_{P}, x\oftp A) \vd P \hastype B \RImp C$ \` By 
sub-derivation\\
$\cE::(\GG,\D'_P\D_{Q});\O;\D_{N}\vd N\hastype A$ \` By 
hypothesis\\
$(\GG,\D_{Q}); \Omega; (\Delta'_{P}, \D_N) \vd [N/x] P \hastype B \RImp C$ \` By 
IH $3$ on $\cD_{1}, \cE$\\
$(\GG,\D_{Q},\D_N); \Omega; \Delta'_{P} \vd [N/x] P \hastype B
\RImp C$ \` By Loosening$^1$ $\D_N$\\
$\cD_2::(\Gamma,\D_{N},x\oftp A,\D'_{P});\Omega;\D_{Q} \vd Q \hastype B$ \` By 
sub-derivation\\
 %$(\Gamma,\D_{N},x\oftp A,\D'_{P},\D_{Q});\Omega;\cdot \vd Q \hastype B$ \` By 
% Loosening$^{1}$\\
 $\cE'::(\GG,\D'_P,\D_Q,\D_N);\O;\cdot\vd N\hastype A$ \`By
 Loosening$^{1}$ $\D_N$ in $\cE$\\
% hypothesis\\
$(\GG,\D_{N},\Delta'_{P}); \Omega; \Delta_{Q} \vd [N/x] Q \hastype B$ \` By 
IH $1$ on $\cD_{2}, \cE'$\\
$\GG;\O;(\Delta'_{P},\D_{Q},\D_{N})\vd[N/x] (P\ Q)^{1}\hastype C$\` By rule
\etab
\item[\textbf{$x\in \D_{Q}$}] Symmetrical to the above.
\enit
\enit
\enen   % 123sub
\end{proof}


\begin{Theorem}[Contraction] 
Let $z$ be a fresh variable of type $A$:
\label{thm:contr}
\begin{enumerate}
\item (Contraction$^{u}$)
If $(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M
\hastype C$, then $(\Gamma, z\oftp A) ;\Omega;\Delta\vd [z/y]([z/x]M) \hastype C$.
\item  (Contraction$^{0}$)
If $\Gamma; (\Omega, x\oftp A, y\oftp A);\Delta \vd M
\hastype C$, then  $\Gamma;(\Omega, z\oftp A);\Delta \vd [z/y]([z/x]M) \hastype C$.
\item  (Contraction$^{1}$)
If $\Gamma;\Omega;(\Delta, x\oftp A, y\oftp A ) \vd M
\hastype C$, then  $\Gamma;\Omega;(\Delta, z\oftp A) \vd [z/y]([z/x]M) \hastype C$.
\end{enumerate}
\end{Theorem}
\begin{proof}
\mbox{}
\ben
\item
\btab
$(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M\hastype C$
\` By assumption\\
$(\Gamma, x\oftp A, y\oftp A,z\oftp A);\Omega;\Delta \vd M\hastype C$
\` By Weakening$^u$\\
$(\Gamma, y\oftp A,\D, z\oftp A);\Omega;\cdot \vd z\hastype A$
\` By rule $Id^u$\\
$(\Gamma, y\oftp A, z\oftp A);\Omega;\Delta \vd [z/x]M\hastype C$
\` By Substitution$^u$\\
$(\Gamma, \D, z\oftp A);\Omega;\cdot\vd z\hastype A$
\` By rule $Id^u$\\
$(\Gamma,  z\oftp A);\Omega;\Delta \vd[z/y] ([z/x]M)\hastype C$
\` By Substitution$^u$
\etab
\item
Similarly, using Substitution$^0$.
\item
\btab
$\Gamma;\Omega;(\Delta, x\oftp A, y\oftp A ) \vd M\hastype C$\ba
$(\Gamma,z\oftp A);\Omega;(\Delta, x\oftp A, y\oftp A ) \vd M\hastype C$
\`By Weakening$^u$\\
$(\Gamma, y\oftp A,\D);\Omega;z\oftp A \vd z\hastype A$
\` By rule $Id^1$\\
$\Gamma;\Omega;(\Delta,y\oftp A, z\oftp A) \vd [z/x]M\hastype C$
\` By Substitution$^1$\\
$(\Gamma,z\oftp A);\Omega;(\Delta, y\oftp A) \vd [z/x]M\hastype C$
\` By Loosening$^1$\\
$(\Gamma,\D);\Omega;z\oftp A \vd z\hastype A$\` By rule $Id^1$\\
 $\Gamma;\Omega;(\Delta, z\oftp A) \vd [z/y]([z/x]M) \hastype C$
\` By Substitution$^1$
\etab
\enen
\end{proof}
 

\smallskip
The notions of reduction and expansion derive directly from the ordinary
$\beta$ and $\eta$ rules.

\[ \begin{array}{rcl}
   (\lam x^k\oftp A\ldot M)\, N^k & \betared & [N/x]M \\
   [1ex]
   M \hastype A \GImp{k} B & \etaexp & \lam x^k\oftp A\ldot M\  x^k \\
\end{array} \]

Indeed one of the main reason to introduce    irrelevant variables, as 
ones which \emph{may} occur but \emph{must not} be used, is to 
well-type $\eta$-expansion of invariant functions:

\[ \begin{array}{rcl}
M \hastype A \GImp{0} B & \etaexp & \lam x^0\oftp A\ldot M\ x^0 \\
\end{array} \]
  
The subject reduction and expansion theorems are an immediate consequence 
of the structural and substitution properties.

\begin{Theorem}[Subject Reduction] \mbox{}
\label{thm:subred}
If $\Gamma;\Omega; \Delta \vd M \hastype A$ and $M \betared M'$ then 
$\Gamma;\Omega; \Delta \vd M' \hastype A$.
\end{Theorem}
\begin{proof}  By cases on $k$:
\ben
\item
Let $M\equiv (\lamb{x^{u}}{B} P)Q^{u}\hastype A$ and
$M'\equiv[Q/x]P$. 
\btab
 $\god\vd (\lamb{x^{u}}{B} P)Q^{u}\hastype A$\bh
$\cE::(\GG,\D);\O;\cdot\vd Q\hastype B$\bv 
$\god\vd \lamb{x^{u}}{B} P\hastype B\TImp A$\bv
 $\cD::(\GG,x\oftp B);\O;\D\vd P\hastype A$\bv
 $\god\vd[Q/x]P\hastype A$\`  By Substitution$^{u}$ on $\cD,\cE$ 
\etab
\item
Let $M\equiv (\lamb{x^{0}}{B} P)Q^{0}\hastype A$ and $M'\equiv[Q/x]P$. 
\btab
 $\god\vd (\lamb{x^{0}}{B} P)Q^{0}\hastype A$\bh
 $\cE::(\GG,\O,\D);\cdot;\cdot\vd Q\hastype B$\bv
$\god\vd \lamb{x^{0}}{B} P\hastype B\ZImp A$\bv 
$\cD::\GG;(\O,x\oftp B);\D\vd P\hastype A$\bv
 $\god\vd[Q/x]P\hastype A$\` By Substitution$^{0}$  on $\cD,\cE$
\etab
\item
Let $M\equiv (\lamb{x^{1}}{B} P)Q^{1}\hastype A$ and $M'\equiv[Q/x]P$.  
\btab
 $\GG;\O;\D\vd (\lamb{x^{1}}{B} P)Q^{1}\hastype A$ and $\D=\D_{P},\D_{Q}$\bh
 $\cE::(\GG,\D_{P});\O;\D_{Q}\vd Q\hastype B$\bv
$(\GG,\D_{Q});\O;\D_{P}\vd \lamb{x^{1}}{B} P\hastype B\RImp A$\bv
$\cD::(\GG,\D_{Q});\O;(\D_{P},x\oftp B)\vd P\hastype A$\bv
 $\GG;\O;(\D_{P},\D_{Q})\vd[Q/x]P\hastype A$\`By Substitution$^{1}$  on $\cD,\cE$ 
\etab
\enen
\end{proof}

\begin{Theorem}[Subject Expansion] \mbox{}
\label{thm:subexp}
If $\Gamma;\Omega; \Delta \vd M \hastype A \GImp{k} B$ and $M \etaexp 
M'$ then $\Gamma;\Omega; \Delta \vd M' \hastype A \GImp{k} B$.
\end{Theorem}
\begin{proof} By cases on $k$:
\ben
\item
\btab
$\god\vd M\hastype A\TImp B$\bh 
 $(\Gamma,x\oftp A);\Omega; \Delta \vd M \hastype A\TImp B$\` By Weakening$^{u}$\\
 $(\Gamma,x\oftp A,\Delta);\Omega;\cdot \vd x\hastype A$ \br $Id^{u}$\\
$(\Gamma,x\oftp A);\Omega; \Delta \vd M\ x^{u} \hastype B$\br   $\TImp E$ \\
$\Gamma;\Omega; \Delta \vd \lxua M\ x^{u} \hastype A\TImp  B$\br $\TImp I$ 
\etab
\item
\btab
 $\god\vd M\hastype A\ZImp B$\bh  
$\Gamma;(\Omega,x\oftp A); \Delta \vd M \hastype A\ZImp B$\`By Weakening$^{0}$  \\
 $(\Gamma,\O,x\oftp 
A,\Delta); \cdot;\cdot \vd x\hastype A$\br  $Id^{u}$\\
$(\Gamma,x\oftp A);\Omega; \Delta \vd M\ x^{0} \hastype B$\br  $\ZImp E$ \\
$\Gamma;\Omega; \Delta \vd \lamb{x^{0}}{A} M\ x^{0} 
\hastype A\ZImp  B$\br  $\ZImp I$ 
\etab
\item
\btab
 $\GG;\O;\D\vd M\hastype A\RImp B$\bh
$(\Gamma,x\oftp A);\Omega; \Delta\vd M 
\hastype A\RImp B$\`  By Weakening$^{u}$ \\
$(\Gamma,\D);\O;x\oftp A\vd x\hastype A$\br  $Id^{1}$\\
$\Gamma;\Omega; (\Delta,x\oftp A) \vd M\ x^{1} \hastype B$\br  $\RImp E$\\
$\Gamma;\Omega; \Delta\vd 
\lamb{x^{1}}{A} M\ x^{1} \hastype A\RImp B$\br  $\RImp I$ 
\etab
\enen
\end{proof}

\newcommand{\red}{\stackrel{\mbox{\tiny{$k$}}}{\mapsto}}


\begin{figure}
\[
\begin{array}{c}
\ianc{}{(\lam x^k\oftp A\ldot M)\, N^k  \betared 
  [N/x]M}{\red\beta}\qquad
\ianc{M\red M'}{\lamb{x^k}{A}M\red\lamb{x^k}{A}M}{\red\lambda}
\vsk
\ianc{M\red Q}{(M\ N)^k\red (Q\ N)^k}{\red\nu}
\qquad
\ianc{N\red Q}{(M\ N)^k\red (M\ Q)^k}{\red\mu}
\end{array}
\]
\caption{Reduction rules for $\lc$}
\label{fig:red}
\end{figure}

We can now give the definition of \emph{reduction} in
Figure~\ref{fig:red}: we write $\red^*$ for the reflexive and
transitive closure of $\red$.

\begin{Theorem}[Subject Reduction with Congruences] \mbox{}
\label{thm:subredcong}
If $\Gamma;\Omega; \Delta \vd M \hastype A$ and $M \red^* M'$ then 
$\Gamma;\Omega; \Delta \vd M' \hastype A$.
\end{Theorem}
\begin{proof}  By induction\fixed on the derivation of  $M\red^*
  M'$, using Subject Reduction (Theorem~\ref{thm:subred}) for the base
  cases.
\end{proof}
% \subsection{Properties of Contexts}

The following Lemma\fixed establishes a sort of consistency property of the
type system,  so that a term can be typed only by exclusive
contexts. In particular we show that a term $M$ cannot be both strict
and vacuous in one variable, say $x$. This will be central in the proof
of disjointness of term complementation (Theorem \ref{thm:part2}):

\begin{Lemma}
\label{le:disj}
It is not the case that both $\GG_1;\O_1;(\D_1,x\oftp C)\vd M\hastype 
A$ and $\GG_2;(\O_2,x\oftp C);\D_2\vd M\hastype A$.
\end{Lemma}
\begin{proof}
  By induction on the structure of $\cD_1::\GG_1;\O_1;(\D_1,x\oftp C)\vd
  M\hastype A$ and inversion on\\
 $\cD_2::\GG_2;(\O_2,x\oftp C);\D_2\vd  M\hastype A$.  
\bit 
\itc
$$\cD_1=\ianc{}{\GG_1;\O_1;x\oftp A\vd x\hastype 
A}{Id^{1}}$$
but there can be no proof of $x\hastype A$ from $\GG_2;(\O_2,x\oftp 
A);\D_2$.
\nitc $Id^u$ and $Con$.
\itc
$$\cD_1= \ianc{\GG_1;\O_1;(\D_1,x\oftp C,y\oftp B)\vd M\hastype  A}
{\GG_1;\O_1;(\D_1,x\oftp C)\vd\lamb{y^{1}}{B} M\hastype B\RImp A}{\RImp I}$$
and
$$\cD_2= \ianc{\GG_2;(\O_2,x\oftp C);(\D_2,y\oftp B)\vd M\hastype  A}
{\GG_2;(\O_2,x\oftp C);\D_2\vd\lamb{y^{1}}{B} M\hastype B\RImp A}{\RImp I}$$
\btab
$\GG_1;\O_1;(\D_1,x\oftp C,y\oftp B)\vd M\hastype  A$
\` By sub-derivation of $\cD_1$\\
$\GG_2;(\O_2,x\oftp C);(\D_2,y\oftp B)\vd M\hastype  A$
\` By inversion on $\cD_2$\\
$\perp$ \` By IH
\etab
\itc
$\cD_1$ ends in $\TImp I,\ZImp I$. The result follows analogously by IH.
\itc
$\cD_1$ ends in $\TImp E,\ZImp E$. The result follows by IH on the leftmost 
sub-derivation.
\itc
$\cD_1$ ends in $\RImp E$: there are two sub-cases:
\bit
\item[\subcase] $\D^1_{M}=\Psi^1_M,\xoc$
$$\cD_1= 
\ibnc{(\Gamma_1, \Delta_N^1); \Omega_1; (\Psi_M^1,x\oftp C) \vd M \hastype A \RImp 
B}{(\Gamma_1, \Psi_M^1,x\oftp C); \Omega_1; \Delta_N^1 \vd N \hastype A}{\Gamma_1; 
\Omega_1; (\Psi_M^1,x\oftp C, \Delta_N^1) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$ 
and 
$$ \cD_2=
\ibnc{(\Gamma_2, \Delta_N^2); (\Omega_2,x\oftp C); \D_M^2 \vd M \hastype A \RImp 
B}{(\Gamma_2, \D_M^2);( \Omega_2,x\oftp C); \Delta_N^2 \vd N \hastype A}{\Gamma_2; 
(\Omega_2,x\oftp C); (\D_M^2, \Delta_N^2) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$
\btab
$(\Gamma_1, \Delta_N^1); \Omega_1; (\Psi_M^1,x\oftp C) \vd M \hastype A \RImp 
B$
 \` By sub-derivation of $\cD_1$\\
$(\Gamma, \Delta_N^2); (\Omega_2,x\oftp C); \D_M^2 \vd M \hastype A \RImp 
B$
\` By inversion  on $\cD_2$\\
$\perp$ \` By IH
\etab
\item[\subcase] $\D^1_{N}=\Psi^1_N,\xoc$: Symmetrically.
\enit %subcase
\enit
\end{proof}

% \begin{Lemma} same G,O,D
% \label{le:disj}
% It is not the case that both $\GG;\O;(\D,x\oftp C)\vd M\hastype 
% A$ and $\GG;(\O,x\oftp C);\D\vd M\hastype A$.
% \end{Lemma}
% \begin{proof}
% By  induction on the height of $\cD::\GG;\O;(\D,x\oftp C)\vd M\hastype 
% A$ and inversion on $\cD'::\GG;(\O,x\oftp C);\D\vd M\hastype A$. Cases
% $Con, Id^u$ are trivially satisfied.
% \bit
% \itc 
% $$\cD=\ianc{}{\GG;\O;x\oftp A\vd x\hastype 
% A}{Id^{1}}$$
% but there can be no proof of $x\hastype A$ from $\GG;(\O,x\oftp 
% A);\cdot$.
% \itc
% $$\cD= \ianc{\GG;\O;(\D,x\oftp C,y\oftp B)\vd M\hastype  A}
% {\GG;\O;(\D,x\oftp C)\vd\lamb{y^{1}}{B} M\hastype B\RImp A}{\RImp I}$$
% and
% $$\cD'= \ianc{\GG;(\O,x\oftp C);(\D,y\oftp B)\vd M\hastype  A}
% {\GG;(\O,x\oftp C);\D\vd\lamb{y^{1}}{B} M\hastype B\RImp A}{\RImp I}$$
% \btab
% $\GG;\O;(\D,x\oftp C,y\oftp B)\vd M\hastype  A$
% \` By sub-derivation of $\cD$\\
% $\GG;(\O,x\oftp C);(\D,y\oftp B)\vd M\hastype  A$
% \` By inversion on $\cD'$\\
% $\perp$ \` By IH
% %$\perp$ \` By rule
% \etab
% \itc
% $\cD$ ends in $\TImp I,\ZImp I$. The result follows analogously by IH.
% \itc
% $\cD$ ends in $\TImp E,\ZImp E$. The result follows by IH on the leftmost 
% sub-derivation.
% \itc
% $\cD$ ends in $\RImp E$: there are several\fixed sub-cases:
% \bit
% \item[\textbf{$x\in\D_{M}$}]\mbox{}
% $$\cD=
% \ibnc{\arv{\cD_1}{(\Gamma, \Delta_N); \Omega; (\Delta'_M,x\oftp C) \vd M \hastype A \RImp 
% B}}{\arv{\cD_2}{(\Gamma, \Delta'_M,x\oftp C); \Omega; \Delta_N \vd N \hastype A}}{\Gamma; 
% \Omega; (\Delta'_M,x\oftp C, \Delta_N) \vd M\ N^1 \hastype B}{\GImp{1}E}
% $$ 
% and 
% $$\cD'=
% \ibnc{\arv{\cD'_1}{(\Gamma, \Delta_2); (\Omega,x\oftp C); \Delta_1 \vd M \hastype A \RImp 
% B}}{\arv{\cD_2'}{(\Gamma, \Delta_1);( \Omega,x\oftp C); \Delta_2 \vd N \hastype A}}{\Gamma; 
% (\Omega,x\oftp C); (\Delta_1, \Delta_2) \vd M\ N^1 \hastype B}{\GImp{1}E}
% $$
% where $\D_1,\D_2=\D'_M,\D_N$:
% \bit
% \item[$\D_2\subseteq\D_N$]
% \btab
% $\cD_1::(\Gamma, \Delta_N); \Omega; (\Delta'_M,x\oftp C) \vd M \hastype A \RImp 
% B$ \` By sub-derivation of $\cD$\\
% $\cD'_1::(\Gamma, \Delta_2); (\Omega,x\oftp C); \Delta_1 \vd M
% \hastype A \RImp B$\` By inversion on  $\cD'$\\ 
% $(\Gamma, \Delta_2); (\Omega,x\oftp C); (\Delta'_M,\D') \vd M
% \hastype A \RImp B$\` as $\D_1\setminus\D'=\D'_M$\\ 
% $(\Gamma, \Delta_2,\D'); (\Omega,x\oftp C); \Delta'_M \vd M
% \hastype A \RImp B$\` By loosening$^1$ $\D'$\\
% $(\Gamma, \Delta_N); (\Omega,x\oftp C); \Delta'_M \vd M\hastype A
% \RImp B$\` as $\D_2,\D'=\D_N$\\
% $\perp$ \` By IH
% \etab
% \item[$\D_N\subseteq\D_2$] Symmetrically.
% \item[$\D_1\subseteq\D_N$] Similarly by Loosening$^1$ $\D'_M$ in
%   $\cD_1$ and $\D_1$ in $\cD'_1$.
% \item[$\D_N\subseteq\D_1$] Symmetrically to the last case.
% \enit
% \item[\textbf{$x\in\D_{N}$}] Symmetrically to $x\in\D_M$.
% \enit %subcase
% \enit
% \end{proof}


\begin{Corollary}[Exclusivity]
\label{co:disj}
\mbox{}\ben
\item
It is not the case that both $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ and 
$(\GG,\O,\D);x\oftp C;\cdot\vd M\hastype A$.
\item
It is not the case that both $\GG;(\O,x\oftp C);\D\vd M\hastype A$ and 
$(\GG,\O,\D);\cdot;x\oftp C\vd M\hastype A$.
\enen
\end{Corollary}
\begin{proof}
\mbox{}
\ben
\item
\btab
It is not the case that  $\GG;\O;(\D,x\oftp C)\vd M\hastype 
A$ and $\GG;(\O,x\oftp C);\D\vd M\hastype A$\` By Lemma \ref{le:disj}\\
It is not the case that  $\GG;\O;(\D,x\oftp C)\vd M\hastype 
A$ and $(\GG,\D);(\O,x\oftp C);\cdot\vd M\hastype A$\` By
Loosening$^1$ $\D$\\
It is not the case that  $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ and 
$(\GG,\O,\D);x\oftp C;\cdot\vd M\hastype A$\` By
Loosening$^0$ $\O$
\etab
\item Analogously.
\enen
\end{proof}

%\newcommand{\er}[1]{\mid #1\mid_{\mbox{\textrm{er}}}}
\newcommand{\er}[1]{\mid #1\mid}

We end this section by checking that our strict calculus is a 
conservative extension of the simply typed $\l$-calculus.  We 
therefore define a forgetful functor from $\lc$ to $\l^{\Imp}$:
\beq
\er{A\GImp{k} B} & = & \er{A}\  \Imp\ \er{B}\\
\er{a} & = & a
\vsk
\er{x} & = & x\\
\er{c} & = & c\\
\er{\lamb{x^{k}}{A} M} & = & \lamb{x}{\er{A}} \er{M}\\
\er{M\ N^{k}} & = & \er{M}\ \er{N}
\vsk
\er{\cdot} & = & \cdot\\
\er{\GG,x\oftp A} & = & \er{\GG}, x\oftp \er{A}\\
\er{\Sigma,a\oftp type} & = & \er{\Sigma}, a\oftp type\\
\er{\Sigma,c\oftp A} & = & \er{\Sigma}, c\oftp \er{A}
\eneq

\begin{Theorem}[Conservativity]
\label{thm:conserv}
\mbox{}\\
If $\god\vd_{\lc}M\hastype A$,, then
$\er{\GG},\er{\O},\er{\D}\vd_{\l^{\Imp}} \er{M}\ \hastype\ \er{A}$.
\end{Theorem}
\begin{proof}
By induction on the structure of the given derivation.
\end{proof}


% HERE CANON
\input{cnn}


\newcommand{\repf}[1]{\rep{#1}}
\bigskip
We will also need the typing  and  the canonical form rule for existential
variables. We use $\Phi$ for arrays of (distinct) labeled bound
variables; if $x^k\in\Phi$, we set $\Phi(x)= k$. We say that
$\god\vd\Phi\ ok$ if the following holds:
\beq
 \Phi(x) = u & \BImp & x\in\dom(\GG)\\
 \Phi(x) = 0 & \BImp & x\in\dom(\O)\\
 \Phi(x) = 1 & \BImp & x\in\dom(\D)\\
\eneq
Moreover, if $\god\vd M\hastype A$ and $\god\vd\Phi\ ok$ we may write
$\repf{\Phi}\vd M \hastype A$.
We assume that the type $A$ in $E_A$ is well-behaved \wrt  $\Phi$.
\beq
%\ianc{\cdot;\cdot;\cdot\vd E_{A}\hastype A}
%{\god\vd E_{A}\ \pi(\GG^u);\pi(\O^0);\pi(\D^1) \hastype P}{Pat}
\ianc{\god\vd\Phi\ ok}{\god\vd E_{A}\ \Phi \hastype a}{Pat}
\qquad
\ianc{\god\vd E_{A}\ \Phi \hastype a}{\god \vd E_{A}\ \Phi \da  a}{cPat}
\eneq


\begin{Remark}
\label{rmk:disj}
Exclusivity (Lemma \ref{le:disj}) holds for open patterns as well.
\end{Remark}
\begin{proof}
  Assume that both $\GG;\O;(\D,x\oftp C)\vd E\ \Phi\hastype A$ and
  $\GG';(\O',x\oftp C);\D'\vd E\ \Phi\hastype A$. Then
  $\GG;\O;(\D,x\oftp C)\vd \Phi\ ok$ and $\GG';(\O',x\oftp C);\D'\vd
  \Phi\ ok$ iff $\Phi(x)=1$ and $\Phi(x)=0$, impossible.
\end{proof}


% HERE RELATED

\input{relatedstrict}

