\begin{lemma}
\label{le:edisj}
It is not the case that $\GG\vd M \in \|E \ x_{1}^{l_{1}}\dots x_{j-1}^{l_{j-1}}\ 
x_{j}^{l_j}\ x_{j+1}^{l_{j+1}}\dots x_n^{l_{n}})\|$
and  entails $\GG\vd M \in \|E \ x_{1}^{u}\dots x_{j-1}^{u}\ 
x_{j}^{-l_j}\ x_{j+1}^{u}\dots x_n^{u)\|$.
\end{lemma}
\newcommand{\oxa}{\Omega,x\oftp A'}
\newcommand{\dxa}{\Delta,x\oftp A'}
\newcommand{\cE}{{\cal E}}
\newcommand{\cD}{{\cal D}}
\begin{proof}
We only consider the case $l_{j }=1$ and we shorten $x_{j}^{1}$ in 
$x^{1}$. We assume to have oppurtunately distributed the x_{1}^{l_{1}}\dots
 x_{j-1}^{l_{j-1}}\ x_{j+1}^{l_{j+1}}\dots x_n^{l_{n}} $ in the right 
 contexts, as well as tyhe $ x_{1}^{u}\dots x_{j-1}^{u}\ 
 x_{j+1}^{u}\dots x_n^{u)$, which ends all in $\GG$. We thus prove 
 that
%  By inversion on rule $grflex$ 
% $\GG\vd M \in \| E_B\ x^1\|$ only if $ M\equiv t \ x^1$ and $\cdot\prv 
% t : B$.  We proceed by absurdum and generalize the statement as 
% follows: 
it is not possible that there is a derivation $\cD:: \Gamma; 
\Omega; \Delta,x\oftp A' \vd M : C$ and a derivation $\cE:: \Gamma; 
\Omega,x\oftp A' ; \Delta \vd M : C$.  We proceed by induction on the 
typing derivation $\cE$.  %\begin{itemize}
%\item Case
 $$ \cE = \ianc{c\oftp C \in \Sigma}{\Gamma; \Omega,x\oftp A'; \Delta \vd c \hastype C}{Con}$$
Impossible as $\Delta$ should be empty.
%\item
$$ \cE = \ianc{}{\Gamma; \Omega,x\oftp A'; \Delta \vd y \hastype C}{Id^u}$$
for a different $y$. Impossible again for the above reason.
%\item
$$  \cE =\ianc{}{\Gamma; \Omega,x\oftp A'; \Delta \vd y \hastype C}{Id^1}$$
for a different $y$. Impossible as $\Delta$ should contain $ y \hastype C$
only.
%\item
No case for $Id^0$ and no case for $y\equiv x$.


%\item
 
$$ \cE = 
\ianc{\cE_{1}:: \Gamma; (\Omega, x\oftp A',y\oftp A); \Delta \vd M \hastype B}{\Gamma;
\Omega, x\oftp A' ; \Delta \vd \lam y^0 \oftp A\ldot M \hastype A \GImp{0}
B}{\GImp{0}I} $$
By inversion on $\cD$, there is a subproof 
$$\cD_{1}:: \Gamma; (\Omega,y\oftp A); (\Delta, x\oftp A') \vd M \hastype 
B$$ By IH on $\cD_{1}$ and $\cE_{1}$, we have the absurdum.
The cases $\GImp{u}I$ and $\GImp{1}I$ are totally analogous.
%\item 
  
$$\cE = 
 \ibnc{\cE_{1}:: \Gamma; \oxa; \Delta \vd M \hastype A \ZImp B}{(\Gamma, 
\oxa); \Delta; \cdot \vd N \hastype A}{\Gamma; \oxa;
\Delta \vd M\, N^0 \hastype B}{\GImp{0}E}$$
By inversion on $\cD$ there is a subproof
$$\cD_{1}:: \Gamma; \Omega; \dxa \vd M \hastype 
B$$ By IH on $\cD_{1}$ and $\cE_{1}$, we have the absurdum.
Analogously for $\GImp{u}E$ as the left antecedent does not change.
%\item
\begin{small}  
$$\cE = 
 \ibnc{\cE_1:: \Gamma; (\oxa, \Delta_N); (\Delta_M, \Delta_{MN}) \vd M
\hastype A \RImp B}{\cE_2::\Gamma; (\oxa, \Delta_M); (\Delta_N, \Delta_{MN})
\vd N \hastype A}{\Gamma; \oxa; (\Delta_M, \Delta_N, \Delta_{MN}) \vd
M\, N^1 \hastype B}{\GImp{1}E}$$
\end{small}

Now the derivation $\cD$ is as follows:
\begin{small}
$$ \cD =
\ibnc{\cD_1::\Gamma; (\Omega, \Delta^{'}_N); (\Delta^{'}_M, \Delta^{'}_{MN}) \vd M
\hastype A \RImp B}{\cD_2::\Gamma; (\Omega, \Delta^{'}_M); (\Delta^{'}_N, \Delta^{'}_{MN})
\vd N \hastype A}{\Gamma; \Omega; (\Delta^{'}_M, \Delta^{'}_N, \Delta^{'}_{MN}) \vd
M\, N^1 \hastype B}{\GImp{1}E}$$
\end{small}
There are three disjoint subcases depending on where $x$ belongs:
\bit
\item Subcase I: $\Delta^{'}_M = \Delta_M, x\oftp A',\Delta^{'}_N = \Delta_N,
\Delta^{'}_{MN} = \Delta_{MN}$. Thus we have
$\cD_1:: \GG;(\Omega,\Delta_N);(\Delta_M, x\oftp A', \Delta_{MN)\vd M\hastype A \RImp B$
and this contradicts $\cE_1$
\item  Subcase II:  $\Delta^{'}_N= \Delta_N, x\oftp A',\Delta^{'}_M= \Delta_M,
\Delta^{'}_{MN} = \Delta_{MN}$. The case is symmetrical to the previous one 
and the contradiction
is obtained from $\cE_2$ and $\cD_2$.
\item  Subcase
III:  $\Delta^{'}_N= \Delta_N ,\Delta^{'}_M= \Delta_M,
\Delta^{'}_{MN} = \Delta_{MN},x\oftp A'$. Then the contradiction comes from
$\cE_i$ and $\cD_i$ for $i=1$ or $2$.      
\enit

\end{proof}
%  main proof 

Basis: $N$ is the flexible term $E\ \ol{x_n^{l}}$.  $\GG \prv M\in 
\|\mnot(E\ \ol{x_n^{l}})\|$ iff there is a $j$ such that $\GG \prv 
M\in\|\mnot(E \ x_{1}^{l_{1}}\dots x_{j-1}^{l_{j-1}}\ x_{j}^{l_j}\ 
x_{j+1}^{l_{j+1}}\dots x_n^{l_{n}})) \|$, where $l_{j}$ is a 
determined label $d$: thus by lemma \ref{le:edisj} $\GG \prv M\in 
\|\mnot(E \ x_{1}^{l_{1}}\dots x_{j-1}^{l_{j-1}}\ x_{j}^{d}\ 
x_{j+1}^{l_{j+1}}\dots x_n^{l_{n}})) \|$ entails $\GG\prv M\not\in 
\|Z\ x_{1}^{u}\dots x_{j-1}^{u}\ x_{j}^{-d}\ x_{j+1}^{u}\dots 
x_n^{u}))\|$.
