
We now describe how to make every term fully applied: this is achieved 
via a translation from the canonical forms of the 
simply-typed $\l$-calculus into  strict types.

\newcommand{\LBimp}{\longleftrightarrow}
\newcommand{\emp}{;\cdot;\cdot}

\begin{figure}
\label{fig:trans}  
\[
\begin{array}{c}
\ianc{}{\GG,\Omega\prv  E\ \pi(\GG) \LBimp 
(\GG,\Omega)\emp\prv  F\ \GG^{u} \ \Omega^{0}}{\mbox{\rm Trn\_Pat}} 
\vsk
\ianc{ \GG,x\oftp A \prv  M \LBimp  \GG,x\oftp A\emp\prv  N }
{\GG\prv \lxa M \LBimp \GG\emp\prv \lamb{x^u}{ N} }{\mbox{\rm Trn\_Lam}}\vsk
\ianc{  \GG\prv  M_{1}  \LBimp \GG\emp\prv N_{1}
\cdots \GG\prv  M_{n} \LBimp \GG\emp\prv N_{n} }
{\GG\prv h\  \Mn \LBimp  \GG\emp\prv h\ \Nn} {\mbox{\rm Trn\_App}}
\end{array}
\]
\caption{Full application Translation}
\end{figure}

To prove the adequacy of the translation, we need as usual the 
following technical Lemma:

\newcommand{\cx}{x\oftp C;\cdot;\cdot}
\newcommand{\cxom}{ x\oftp C;\Omega;\cdot}

\begin{Lemma}
\label{le:fat}
\mbox{}
\ben
\item
 $\cx\vd M\da A$ iff $\cxom\vd M\da A$.
\item
$\cx\vd M\bua A$ iff $\cxom\vd M\bua A$.
\enen
\end{Lemma}

\begin{proof}
($\Imp$). By simultaneous induction on $\cD_{1}::\cx\vd M\da A$ and $\cD_{2}::\cx\vd M\bua A$.
\bit
\item 
$$\cD = \ianc{c\oftp A\in\Sigma}{\cx \prv  c\da A}{cIdc}$$

$$\cE= \ianc{c\oftp A\in\Sigma}{\cxom \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{\cx\prv  M\da P}{\cx \prv  M\bua P} {cAt}$$
By inversion $\cx\prv  M\da P$, by HI  $\cxom \prv  M\da 
P$ and hence   $\cxom \prv  M\bua P$
\item
$$\cD = \ianc{y\oftp A,\cx \prv M\bua B}{\cx\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
By inversion $y\oftp A,\cx \prv M\bua B$ which entails by IH 
 $y\oftp A,\cxom \prv M\bua B$ and   $\cxom\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$.
\item
$$\cD = \ibnc{\cx \vd M \da A \RImp B}{\cx \vd N \bua A}{\cx \vd
M\, N^1 \da B}{c\RImp E}$$
By inversion there are derivations $\cD_{1}:: \cx \vd M \da A \RImp 
B$ and $\cD_{2}:: \cx \vd N \bua A$. By HI there are derivations 
$\cE_{1}:: \cxom \vd M \da A \RImp B$ and $\cE_{2}:: \cxom \vd N \bua A$; 
by rule $c\RImp E$ we conclude $\cxom\vd M\ N^{1}\da B$.
 \enit
 The other direction is analogous.
\end{proof}

\begin{Ppn}
\label{ppn:fat}
For $N$ a simple term (in canonical form) such that $\GG \vd N 
\LBimp \GG\emp\vd Q$, we have that $\GG\vd M\in\|N\|$ iff $\GG\emp M\in 
\|Q\|$.
\end{Ppn}
\begin{proof}
A straightforward induction on $N$ using  Lemma \ref{le:fat} generalized
to finite $\GG$ at the base case.
\end{proof}
