\newcommand{\whr}{\stackrel{\mbox{\tiny  $whr^k$}}{\longrightarrow}}
\newcommand{\lsb}{ \mbox{[}}
\newcommand{\byind}{\begin{proof} By induction on the structure of 
the given derivation(s).\end{proof}}
\newcommand{\den}[1]{\lsemantics#1\rsemantics}   
\newcommand{\lsemantics}{\mathopen{\lbrack\mkern-3mu\lbrack}}
\newcommand{\rsemantics}{\mathclose{\rbrack\mkern-3mu\rbrack}}

\section{The Canonical Form Theorem}
\label{sec:canonthm}


In this section we establish the existence of canonical forms for
$\lc$, \ie $\beta$-normal $\eta$-long forms, which is crucial for our
intended application. We prove this by Tait's method of \emph{logical
  relations}; we essentially follow the account in
\cite{Pfenning94un}, with a surprisingly little amount of generalization from simple to
strict types; we do differ on the account of substitutions.

We start by presenting the inductive definition of \emph{canonical}
forms in $\lc$.  It is realized by the two mutually recursive
judgments depicted in Figure~\ref{fig:canon}:
\ben 
\item$\GG;\Omega;\Delta\prv M \da A$\qquad $M$ is atomic of type $A$.
\item$\GG;\Omega;\Delta\prv M \bua A$\qquad $M$ is canonical of type $A$.
\enen

\begin{figure}
\[
\begin{array}{c}
\ianc{c\oftp A\in\Sigma}{\GG; \Omega;\cdot  \prv  c\da A}{cIdc}\vsk
\ianc{}{(\GG,x\oftp A);\Omega; \cdot  \prv  x\da A}{cId^{u}}
\qquad \mbox{\textrm{no rule for }}cId^{0}
\qquad
\ianc{}{\GG;\Omega; x\oftp A \prv  x\da A} {cId^{1}}
\vsk
%\ianc{}{\GG;\Omega;\Delta\vd E\ \ol{x_{n}^{l}}\da P}{cPat}
%\qquad
\ianc{\GG;\Omega;\Delta \prv  M\da a}{\GG;\Omega;\Delta \prv  M\bua a} 
{cAt}\vsk
\ianc{(\GG,x\oftp A) ; \Omega;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^u}{A} M) \bua 
A\TImp B} {c\TImp I}
\vsk
\ianc{\GG ; \Omega; (\Delta,x\oftp A) \prv M\bua B}{\GG;\O;\Delta\prv(\lamb{x^1}{A} M) \bua 
A\RImp B}{c\RImp I}
\vsk
\ianc{\GG ;(\Omega, x\oftp A) ;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^0}{A} M) \bua 
A\ZImp B}{c\ZImp I}
\vsk
 \ibnc{\Gamma; \Omega; \Delta \vd M \da A \TImp B}{(\Gamma, \Delta);
\O; \cdot \vd N \bua A}{\Gamma; \Omega; \Delta
\vd M\ N^u \da B}{c\GImp{u}E}
\vsk
\ianc{\GG;\Omega;\Delta\prv M \da A \ZImp B \quad (\GG,\Omega,\Delta);\cdot;\cdot \prv N \bua A
} {\GG;\Omega;\Delta \prv M \ N^0 \da B}{c\ZImp E}\vsk
\ibnc{(\Gamma, \Delta_N); \Omega; \Delta_M \vd M \da A \RImp 
B}{(\Gamma, \Delta_M); \Omega; \Delta_N \vd N \bua A}{\Gamma; \Omega;
(\Delta_M, \Delta_N) \vd M\ N^1 \da B}{c\RImp E}
\end{array}
\]
\caption{Canonical forms}
\label{fig:canon}
\end{figure}



\begin{figure}
\[
\begin{array}{c}
\ianc{c\oftp A\in\Sigma}{\Psi \prv  c\da c\hastype A}{tcIdc}\qquad
%\ianc{}{\Psi\prv  x\da x\hastype A}{tcId^{u}}
%\qquad \mbox{\textrm{no rule for }}tcId^{0}
\qquad
\ianc{x\oftp A\in\Psi}{\Psi \prv  x\da x\hastype A} {tcIdvar}
\vsk
\ibnc{M\whr M'}{\Psi\vd M'\bua M''\hastype a}{\Psi\vd M\bua M''\hastype a}{tc
\whr}
\qquad
\ianc{\Psi \prv  M\da N\hastype a}{\Psi\prv
  M\bua N\hastype a} {tc\atm}
\vsk
\ianc{\Psi \prv M\ x^k\bua N\hastype B}
{\Psi\prv M\bua (\lamb{x^x}{A} N) \hastype A\GImp{k} B}
{tc\GImp{k} I}
\qquad
% \ianc{\GG ;(\Omega, x\oftp A) ;\Delta \prv M\ x^0\bua N\hastype B}
% {\GG;\Omega;\Delta\prv M\bua (\lamb{x^0}{A} N) \hastype A\ZImp B}{tc\ZImp I}
% \vsk
% \ianc{\GG ; \Omega; (\Delta,x\oftp A) \prv M\ x^1\bua N\hastype B}
% {\GG;\Delta\prv M\bua(\lamb{x^1}{A} N) \hastype A\RImp B}{tc\RImp I}
% \vsk
 \ibnc{\Psi\vd M \da P\hastype A \GImp{k} B}{\Psi \vd N \bua Q
 \hastype A}{\Psi \vd M\ N^k \da P\ Q^k\hastype B}{tc\GImp{k}E}
% \vsk
% \ibnc{\GG;\Omega;\Delta\prv M \da P\hastype A \ZImp B}{ (\GG,\Omega,\Delta);
% \cdot;\cdot \prv N \bua Q\hastype A}
% {\GG;\Omega;\Delta \prv M \ N^0 \da P\ Q^0\hastype B}{tc\ZImp E}\vsk
% \ibnc{(\Gamma, \Delta_N); \Omega; \Delta_M \vd M \da P\hastype A \RImp 
% B}{(\Gamma, \Delta_M); \Omega; \Delta_N \vd N \bua Q\hastype
% A}{\Gamma; \Omega; (\Delta_M, \Delta_N) \vd M\ N^1 \da P\ Q^1\hastype
% B}{tc\RImp E}
\end{array}
\]
\caption{Conversion to canonical form}
\label{fig:tocanon}
\end{figure}

\begin{Lemma}[Soundndess of  Canonical Terms]
\label{le:conversound}
 If $\god\vd M\buda A$, then $\god\vd M\hastype A$.
\end{Lemma}
\begin{proof}
 By induction on the structure of the derivation of $\god\vd
  M\buda A$.
\end{proof}
We then introduce \emph{conversion} to canonical form in
Figure~\ref{fig:tocanon}. Note that conversion is not required to
respect the occurrence constraints, provided that we start with a
well-typed term:
\ben 
\item $\Psi\prv M \da N\hastype A\qquad M$ converts to 
 atomic form $N$ at  type $A$.
\item$\Psi\prv M \bua N\hastype A\qquad M$ converts to
 canonical form $N$ at type $A$.
\enen

 This utilizes weak head reduction, which
includes local reduction ($\beta$) and partial congruence ($\nu$):
\beq
\ianc{}{(\lamb{x^k}{A}M)N^k\whr[N/x]M}{\beta}\qquad
\ianc{M\whr Q}{(M\ N)^k\whr (Q\ N)^k}{\nu}
\eneq

\newcommand{\godc}{(\GG,\O,\D)}
\begin{Theorem}[Conversion Yields Canonical Terms]\mbox{}
\label{thm:convercf}
 If $\godc\vd M\buda N\hastype A$ and $\god\vd M\hastype A$, then $\god\vd N\buda A$.
\end{Theorem}
\begin{proof}
 By induction on the structure of $\cD::\godc\vd M\buda N\hastype A$
  and inversion on the typing derivation;   we show some cases:
\bit
\itc
$$\cD=\ianc{x\oftp A\in\Psi}{\Psi \prv  x\da x\hastype A} {tcIdvar}
$$
\bit
\item[\subcase] $$\ianc{}{\GG;\O;\xoa\vd x\hastype A}{Id^1}$$ Then: 
$$\ianc{}{\GG;\Omega; x\oftp A \prv  x\da A} {cId^{1}}$$
\item[\subcase] $$\ianc{}{(\GG,\xoa);\O;\cdot\vd x\hastype A}{Id^u}$$ Then: 
$$\ianc{}{(\GG,\xoa);\Omega; \cdot \prv  x\da A} {cId^{u}}$$
\enit
\itc
$$\cD=\ibnc{M\whr M'}{\Psi\vd M'\bua M''\hastype a}{\Psi\vd M\bua
  M''\hastype a}{tc\whr}$$
\btab $\god\vd M\hastype a$\bh $\god\vd
M'\hastype a$\`By subject reduction
(Theorem~\ref{thm:subred})\\
$\god\vd M''\bua a$\bi
 \etab 
\itc
$$\cD= \ibnc{\Psi\vd M \da P\hastype A \GImp{k} B}{\Psi \vd N \bua Q
 \hastype A}{\Psi \vd M\ N^k \da P\ Q^k\hastype B}{tc\GImp{k}E}$$
\bit
\item[\subcase]
$$\cD'= \ibnc{\Gamma; \Omega; \Delta \vd M \hastype
 A \TImp B}{(\Gamma, \Delta);
\O; \cdot \vd N \hastype A}{\Gamma; \Omega; \Delta
\vd M\ N^u \hastype B}{E\GImp{u}E}$$
\btab
$\Gamma; \Omega; \Delta \vd P \da A \TImp B$\bi\\
$(\Gamma, \Delta);\O; \cdot \vd Q\bua A$\bi\\
$\Gamma; \Omega; \Delta\vd P\ Q ^u \da B$\br
\etab
\item[\subcase] $\cD'$ is $E\GImp{0}E,E\GImp{1}E$: analogously.
\enit

\enit
\end{proof}

Since we have to talk about open terms, we will need a notion of
context extension:
\beq
\ianc{}{\Psi\geq\Psi}{}\qquad
\ianc{\Psi'\geq\Psi}{\Psi',\xoa\geq\Psi}{}
\eneq

\begin{Lemma}[Weakening for Conversion to Canonical and Atomic Form]
\label{le:tcweak}
\mbox{}\\
 If $\Psi\vd M\buda N\hastype A$ and $\Psi'\geq\Psi$, then $\Psi\vd
M\buda N\hastype A$.
\end{Lemma}
\byind

We can now introduce \emph{logical relations}, in complete analogy with
the usual definition for the simply-typed $\l$-calculus:


\begin{Definition}[Logical Relations]
\mbox{}
\begin{itemize}
\item[$1.$]
$\Psi\vd M\in\den{a}$ iff $\Psi\vd M\bua N\hastype A$, for some $N$.
\item[$2^k.$]
$\Psi\vd M\in\den{A\GImp{k} B}$ iff for every $\Psi'\geq \Psi$ and every
$N$, if $ \Psi'\vd N\in\den{A}$, then $\Psi'\vd M\
N^k\in\den{B}$.
\end{itemize}
\end{Definition}

%% not needed anymore?
%\begin{Lemma}[Weakening for Logical Relations]
%\label{le:lrweak}
% If $\god\vd M\in\den{A}$ and $\GG'\geq\GG$, then $\GG';\O;\D\vd
%M\in\den{A}$.
%\end{Lemma}
%\begin{proof}
%By induction on $A$.
%\end{proof}

\begin{Lemma}\mbox{}
\label{le:lr2canon}
\ben
\item If $\Psi\vd M\in\den{A}$, then $\Psi\vd M\bua N\hastype A$.
\item If  $\Psi\vd M\da N\hastype A$, then $\Psi\vd M\in\den{A}$.
\enen
\end{Lemma}
\begin{proof}
By induction on $A$.
\bit
\itc $A=a$. Immediate from definition.
\itc $A=A\GImp{k} B$.
\ben
\item %1
\btab
$\Psi\vd M\in\den{A\GImp{k} B}$\bh
$\Psi,\xoa\geq \Psi$\br\\
$(\Psi,\xoa)\vd x\da x\hastype A$\br\\
$(\Psi,\xoa)\vd x\in\den{A}$\bi $2$\\
$(\Psi,\xoa)\vd M\ x^k\in\den{ B}$\bd of $\den{\cdot}$\\
$(\Psi,\xoa)\vd M\ x^k\bua N\hastype B$\bi $1$\\
$\Psi\vd M\bua\lamb{x^k}{A}N\hastype A\GImp{k} B$\br
\etab
\item %2
\btab
$\Psi\vd M\da M_+\hastype A\GImp{k} B$\bh
$\Psi'\geq\Psi$ and $\Psi'\vd N\in\den{A}$\ba
$\Psi'\vd N\bua N_+ \hastype {A}$\bi $1$\\
$\Psi'\vd M\da M_+\hastype A\GImp{k} B$\bl{le:tcweak}
$\Psi'\vd M\ N^k\da M_+ N_+^k\hastype B$\br\\
$\Psi'\vd M\ N^k\in\den{ B}$\bi $2$\\
$\Psi\vd M\in\den{A\GImp{k} B}$\bd  of $ \den{\cdot}$ 
\etab
\enen
\enit
\end{proof}

\begin{Lemma}[Closure under Head Expansion]
\label{le:clohead}
\mbox{}\\
If $\Psi\vd M'\in\den{A}$ and $M\whr M'$, then $\god\vd M\in\den{A}$.
\end{Lemma}
\begin{proof} By induction on $A$:
\bit
\itc   $A=a$; immediate by definition and rule $tc\whr$.
\itc  $A=A\GImp{k} B$:
\btab
$\Psi\vd M'\in\den{A\GImp{k} B}$\bh
$\Psi'\vd N\in\den{A}$ for $\Psi'\geq \Psi$\ba
$\Psi'\vd M'\ N^k\in\den{A}$\bd\\
$(M\ N)^k\whr (M'\ N)^k$\br $\nu$\\
$\Psi'\vd M\ N^k\in\den{A}$\bi\\
$\Psi\vd M\in\den{A\GImp{k} B}$\bd
\etab
%\itc  $A=A\TImp B,A\ZImp B$: similarly.
\enit
\end{proof}


%%%\subsection{Substitutions}
\newcommand{\tri}{\theta}
\newcommand{\trip}{\theta'}
\newcommand{\tripp}{\theta''}
\newcommand{\eps}{\epsilon}

Due to the need to $\beta$-reduce during conversion to canonical form,
we need to introduce
%well-typed 
\emph{substitutions}. Differently from
\cite{Pfenning94un} and \cite{Cervesato99pllf}, we will not require 
substitutions to be well-typed.

\[ \begin{array}{rrcl}
\mbox{\textit{Substitutions}}& \theta & \bnfas \epsilon\bnfalt \theta,M/x
\end{array}
\]
For $\theta=\theta',M/x$, we say that $x$ is \emph{defined} in $\theta$
and we write $\q(x)=M$.  We require all variables defined in a
substitution to be distinct: we use \dom($\theta$) for the set of variables
defined in $\theta$ and cod($\theta$) for the variables occurring in the
substituting terms. We assume them to be disjoint.
% Well-typed
% substitutions are defined as follows:
% \[
% \begin{array}{c}
% \ianc{}{\GG';\O';\cdot
% \vd(\epsilon;\epsilon;\epsilon)\hastype(\cdot;\cdot;\cdot)}
% {\epsilon\cdot}\vsk
% %\ianc{}{\godp\vd\epsilon}{\epsilon}\qquad
% \ibnc{(\GG';\D');\O';\cdot\vd M\hastype A}{\godp\vd\tri\hastype\god}
% {\godp\vd(\gamma,M/x);\omega;\delta\hastype(\GG,x\oftp A);\O;\D} {\tri^u}\vsk
% \ibnc{(\GG';\O';\D');\cdot;\cdot\vd M\hastype A}{\godp\vd\tri\hastype\god}
% {\godp\vd\gamma;(\omega,M/x);\delta\hastype\GG;(\O,\xoa);\D} {\tri^0}\vsk
% \ibnc{(\GG,\D_2);\O;\D_1\vd M\hastype A}{(\GG,\D_1);\O;\D_2\vd\tri\hastype\god}
% {\GG;\O;(\D_1,\D_2)\vd\gamma;\omega;(\delta,M/x)\hastype\GG;\O;(\D,\xoa)} {\tri^1}
% \end{array}
% \]

Next, we define the \emph{application} of a substitution to a term
$M$, denoted $[\tri]M$.
We limit application of substitution to objects whose free variables
are in the domain of $\tri$:
%. Assume $\god\vd M\hastype A$ and $\godp\vd\tri\hastype\god$
 % we write $x^u$ to say that $x$ is
% specifically declared in $\GG$; similarly for the other labels. Define
\beq
[\tri] c & = & c \\ 
% \lsb\tri]  \mbox{$x^u$} & = & \gamma(x)\\
% \lsb\tri] x^0 & = & \omega(x)\\
% \lsb\tri] x^1 & = & \delta(x)\\
\lsb\tri] x & = & \tri(x)\\
\lsb\tri](M\ N^k) & = & ([\tri]M) \ ([\tri] N)^k\\ %%% from Iliano
% \lsb\tri](M\ N^u) & = & ([\tri]M) \ ([(\gamma,\delta);\omega;\epsilon] N)^u\\
% \lsb\tri](M\ N^0) & = & ([\tri]M) \ 
% ([(\gamma,\omega,\delta);\epsilon;\epsilon] N)^0\\
% \lsb\gamma;\omega;(\delta_M,\delta_N)](M\ N^1) & = &
% ([(\gamma,\delta_N);\omega;\delta_M]M) \ ([(\gamma,\delta_M);\omega;\delta_N] N)^1\\
\lsb\tri](\lamb{x^k}{A}M) & = & \lamb{x^k}{A}[\theta,x/x]M
\eneq
Note that in the lambda case we can assume with no loss of generality
that $x$ does not occur in $\dom(\tri)\cup\mbox{cod}(\tri)$.


We will also need to mediate between single-step substitutions stemming
from $\beta$-reduction and simultaneous substitutions.
We  define how to \emph{compose} single step bindings from a
$\beta$ reduction with simultaneous 
 substitutions: 
\beq
[N/x] \eps & = & \eps\\
\lsb N/x] \theta & = & [N/x]\theta,
([N/x]M)/y
\eneq% if

\begin{Lemma}
\label{le:comptheta}
 $[[N/x]\theta]M = [N/x]([\tri]M)$.
\end{Lemma}
\begin{proof}
By induction on the structure of $M$.
\end{proof}

\begin{Corollary}
\label{co:comptheta} Assume $x$ to be fresh in $\tri$:
 $[N/x] ([\theta,x/x]M)= [\theta,N/x]M$.
\end{Corollary}
\begin{proof}
\mbox{}
\btab
$[N/x] ([\theta,x/x])M=$\bh
$ [[N/x](\theta,x/x)])M=$\bl{le:comptheta}
$ [[N/x]\theta,([N/x]x)/x)])M=$\`By composition of
substitution\\
$ [\theta,N/x]M$\`By application of substitution and $x$ fresh
\etab
\end{proof}
\begin{sloppy}
For a context $\Psi=x_1\oftp A_1,\mdots x_n\oftp A_n$, we introduce the
\emph{identity} substitution on $\Psi$ as $id_{\Psi}=x_1/x_1\mdots
x_n/x_n$.
\end{sloppy}
%Define $id_{\god}$ as $id_{\GG};id_{\O};id_{\D}$.% We assume without
%explicit statement and proof the obvious properties of the identity
%substitution, namely that it is a left-unit for the typing judgements,
%as well as for substitution application and composition.

\begin{Lemma}[Identity Substitution]\mbox{}
\label{le:idM}
% \ben
% \item
 If $\god\vd M\hastype A$, then $[id_{\godc}] M= M$.
% \item If $\god\vd [\gamma';\omega';\delta']\hastype \godp$, then 
%$[id_{\god}]\gamma';\omega';\delta' = \gamma';\omega';\delta'$.
%\enen
\end{Lemma}
 \begin{proof}
% \mbox{}
% \ben
% \item
 By induction on $M$.
\end{proof}
\smallskip

We extend the notion of logical relations to contexts, exactly as in the simply
 typed case: a substitution
$\tri$ is in the relation $\den{\Psi}$ if for every binding $M/x$ such
that $x\oftp A$ is in $\Psi$, then $M$ is in $\den{A}$.

\begin{Definition}\mbox{}
\bit
\item[$1$.] $\Phi\vd \theta\in\den{\cdot}$ iff $\theta=\eps$.
\item[$2$.] ${\Phi\vd\theta\in\den{(\Psi,x\oftp A)}
}$ iff $\theta=\theta',M/x$, ${\Phi\vd M\in\den{ A}}$ and
${\Phi\vd\theta'\in\den{\Psi}}$.
\enit
\end{Definition}

We remark that contexts are \emph{not} ordered, hence, for
$\Psi=\godc$ we will identify, for example, 
 $\den{\Psi,\xoa}$ with $\den{(\GG,\xoa,\O,\D)}$.

\begin{Lemma}[Weakening for Logical Relations]
\label{le:lrthetaweak}
If $\Psi\vd \tri\in\den{A}$, then $(\Psi,\xoa)\vd
\tri\in\den{A}$.
\end{Lemma}
\begin{proof}
By induction on the structure of the given derivation.
\end{proof}

\begin{Lemma}[Well-typed Terms are in the Logical Relation]
\label{le:lrmain}
If $\god\vd M\hastype A$, then for every $\Phi$ such that
$\Phi\vd\tri\in\den{\godc}$, $\Phi\vd [\tri]M\in\den{A}$.
\end{Lemma} 
\begin{proof}
By induction on the typing derivation $\cD::\god\vd M\hastype A$:
\bit
\itc $$\cD= \ianc{}{(\Gamma, x\oftp A); \Omega; \cdot \vd x \hastype A}{Id^u}$$
\btab
$\Phi\vd\tri\in\den{(\GG,\xoa,\O)}$\ba
$\Phi\vd\theta(x)\in\den{A}$\bd of $\den{\cdot}$\\
$\Phi\vd[\tri]x\in\den{A}$\bd of substitution
\etab
\itc $$\cD= \ianc{}{\Gamma; \Omega; \xoa \vd x \hastype A}{Id^1}$$
\btab
$\Phi\vd\tri\in\den{(\GG,\O,\xoa)}$\ba
$\Phi\vd\theta(x)\in\den{A}$\bd of $\den{\cdot}$\\
$\Phi\vd [\tri]x\in\den{A}$\bd of substitution.
\etab
\itc $$\cD= \ianc{c\oftp A \in \Sigma}{\Gamma; \Omega; \cdot \vd c \hastype
 A}{Con}$$
Immediate by Lemma~\ref{le:lr2canon} and definition of substitution.
\itc % TImp
$$\cD=\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}$$
\btab
$(\Gamma, x\oftp A); \Omega; \Delta \vd M \hastype B$\bs
$\Phi\vd\tri\in\den{\godc}$\bh 
$\Phi'\geq\Phi$ and 
%% $(\GG',\D');\O';\cdot\vd \tri\in\den{\god}$\bl{le:loosectx}
$\Phi'\vd N\in\den{A}$\ba
$\Phi'\vd(\theta,N/x)\in\den{(\GG,\xoa,\O,\D)}$\bd of $\den{ \cdot  }$
and Weakening (Lemma~\ref{le:lrthetaweak})\\
$\Phi'\vd [ \theta,N/x]M\in\den{B}$\bi \\
$\Phi'\vd [N/x]([\theta,x/x]
M)\in\den{B}$\`By Corollary~\ref{co:comptheta}\\ 
$\Phi'\vd(\lamb{x^u}{A}[\theta,x/x]M) N^u\in\den{B}$\bl{le:clohead}
$\Phi'\vd ([\tri](\lamb{x^u}{A}M)) N^u\in\den{B}$\bd of substitution \\
$\Phi\vd [\tri](\lamb{x^u}{A}M)\in\den{A\TImp B}$\bd of $\den{A\TImp B}$
\etab

\itc % ZImp
$$\cD=\ianc{\Gamma; (\Omega,\xoa); \Delta \vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^0 \oftp A\ldot M \hastype A \GImp{0}
B}{\GImp{0}I}$$
\btab
$\Gamma; (\Omega,\xoa); \Delta \vd M \hastype B$\bs
$\Phi\vd\tri\in\den{\godc}$\bh 
$\Phi'\geq\Phi$ and 
%% $(\GG',\D');\O';\cdot\vd \tri\in\den{\god}$\bl{le:loosectx}
$\Phi'\vd N\in\den{A}$\ba
$\Phi'\vd(\theta,N/x)\in\den{(\GG,\O,\xoa,\D)}$\bd of $\den{ \cdot  }$
and Weakening (Lemma~\ref{le:lrthetaweak})\\
$\Phi'\vd [ \theta,N/x]M\in\den{B}$\bi \\
$\Phi'\vd [N/x]([\theta,x/x]
M)\in\den{B}$\`By Corollary~\ref{co:comptheta}\\ 
$\Phi'\vd(\lamb{x^0}{A}[\theta,x/x]M) N^0\in\den{B}$\bl{le:clohead}
$\Phi'\vd ([\tri](\lamb{x^0}{A}M)) N^0\in\den{B}$\bd of substitution \\
$\Phi\vd [\tri](\lamb{x^0}{A}M)\in\den{A\ZImp B}$\bd of $\den{A\ZImp B}$
\etab

\itc %% RIMP
$$\cD=\ianc{\Gamma; \Omega; (\Delta,\xoa) \vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^1 \oftp A\ldot M \hastype A \GImp{1}
B}{\GImp{1}I}$$
\btab
$\Gamma; \Omega; (\Delta,\xoa) \vd M \hastype B$\bs
$\Phi\vd\tri\in\den{\godc}$\bh 
$\Phi'\geq\Phi$ and 
%% $(\GG',\D');\O';\cdot\vd \tri\in\den{\god}$\bl{le:loosectx}
$\Phi'\vd N\in\den{A}$\ba
$\Phi'\vd(\theta,N/x)\in\den{(\GG,\O,\D,\xoa)}$\bd of $\den{ \cdot  }$
and Weakening (Lemma~\ref{le:lrthetaweak})\\
$\Phi'\vd [ \theta,N/x]M\in\den{B}$\bi \\
$\Phi'\vd [N/x]([\theta,x/x]
M)\in\den{B}$\`By Corollary~\ref{co:comptheta}\\ 
$\Phi'\vd(\lamb{x^1}{A}[\theta,x/x]M) N^1\in\den{B}$\bl{le:clohead}
$\Phi'\vd ([\tri](\lamb{x^1}{A}M)) N^1\in\den{B}$\bd of substitution \\
$\Phi'\vd [\tri](\lamb{x^1}{A}M)\in\den{A\RImp B}$\bd of $\den{A\RImp B}$
\etab
%%%% end intro rules
\itc
$$\cD= \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}$$
\btab
$\Phi\vd\tri\in\den{\godc}$\bh
$\Gamma; \Omega; \Delta \vd M \hastype A \UImp B$\bs
$\Phi\vd[\tri]M\in\den{A\TImp B}$\bi\\
$(\Gamma,\Delta); \Omega; \cdot \vd N \hastype A$\bs
$\Phi \vd [\tri]N \in\den{ A}$\bi\\
$\Phi\geq\Phi$\br\\
$\Phi\vd ([\tri]M)([\tri] N)^u\in\den{B}$\bd
of $\den{ \cdot  }$\\ 
$\Phi\vd [\tri](M\ N)^u\in\den{B}$\bd of substitution
\etab
%%%% ZIMP
\itc
$$\cD= \ibnc{\Gamma; \Omega; \Delta \vd M \hastype A \ZImp B}{(\Gamma,
  \O,\Delta); \cdot; \cdot \vd N \hastype A}{\Gamma; \Omega; \Delta
  \vd M\ N^0 \hastype B}{\GImp{0}E}$$
\btab
$\Phi\vd\tri\in\den{\godc}$\bh 
$\Gamma; \Omega; \Delta \vd M \hastype A \ZImp B$\bs
$\Phi\vd[\tri]M\in\den{A\ZImp B}$\bi\\
$(\Gamma,\Omega,\Delta); \cdot; \cdot \vd N \hastype A$\bs
$\Phi \vd [\tri]N \in\den{ A}$\bi\\
$\Phi\geq\Phi$\br\\
$\Phi\vd ([\tri]M)([\tri]N)^0\in\den{B}$\bd of $\den{ \cdot  }$\\
$\Phi \vd [\tri](M\ N)^0\in\den{B}$\bd of substitution 
\etab
% \btab
% $\Gamma; \Omega; \Delta \vd M \hastype A \ZImp B$\bs
% $\godc\vd[\tri]M\in\den{A\ZImp B}$\bi\\
% $(\Gamma,\O,\Delta); \cdot; \cdot \vd N \hastype A$\bs
% $(\Gamma,\O,\Delta); \cdot; \cdot \vd N \in\den{ A}$\bi\\
% $\O\geq\O$\br\\
% $\godc\vd ([\tri]M)([\tri] N)^0\in\den{B}$\bd of $\den{ \cdot  }$\\
% $\god\vd [\tri](M\ N)^0\in\den{B}$\bd of substitution
% \etab
\itc
$$\cD=\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}$$
\btab
 $\Phi\vd\tri\in\den{(\GG,\O,\dmn)}$\bh
 $(\Gamma,\D_N); \Omega; \Delta_M \vd M \hastype A \RImp B$\bs
 $\Phi\vd[\tri]M\in\den{A\RImp B}$\bi\\
 $(\Gamma,\Delta_M); \O; \D_N \vd N \hastype A$\bs
 $\Phi \vd N \in\den{ A}$\bi\\
 $\Phi\geq\Phi$\br\\
 $\Phi\vd ([\tri]M)([\tri] N)^1\in\den{B}$\bd of $\den{ \cdot  }$\\
 $\Phi\vd [\tri](M\ N)^1\in\den{B}$\bd of
 substitution \etab \enit
\end{proof}

\begin{Lemma}
\label{le:lrid}
 $\Psi\vd id_{\Psi}\in\den{\Psi}$. 
\end{Lemma}
\begin{proof}
  By a straightforward induction on $\Psi$ using
  Lemma~\ref{le:lr2canon}(2).
\end{proof}


\begin{Theorem}[Canonical Form Theorem]
\label{thm:canonical}
 If $\god\vd M\hastype A$, then there is $N$ such that $\godc\vd
  M\bua N\hastype A$ and $\god\vd N\bua A$.
 
\end{Theorem}
\begin{proof}
  Assume $\god\vd M\hastype A$: By Lemma \ref{le:lrid} $ \godc\vd
  id_{\godc}\in\den{\godc}$, hence, by Lemma \ref{le:lrmain} $\godc\vd
  [id_{\godc}]M\in\den{A}$ and thus by Lemma~\ref{le:idM} $\godc\vd
  M\in\den{A}$; by Lemma \ref{le:lr2canon}(1), $\godc\vd M\bua
  N\hastype A$ for some $N$. Additionally, by Theorem~\ref{thm:convercf}(2)
  $\god\vd  N\buda A$.
\end{proof}

We shall abbreviate the statement of the canonical form Theorem as
$\GG;\Omega;\Delta\prv M \buda A$.

