\begin{Theorem}
\label{thm:part2}
Assume $\GG\vd N\hastype A$ is simple linear pattern; then, either
$\GG \prv M\in \| N \| \hastype A$ or and there is a $Q$ such that
$\GG\vd \mnot(N)\blip Q\hastype A$ and $ \GG \prv M\in \| Q\| \hastype
A$.
\end{Theorem}
\begin{proof}
  By induction on the structure of $N$ and inversion on  $\cD::\GG\vd
  \mnot(N)\blip   Q\hastype A$.
\bit
\itc $\cD$ ends in $\mnot\_Flx$.
%   Again observe that $E\ 
% \ol{x_{n}^{l}}$ can be seen as $E\ \Phi^{u}\Omega^{0}\Delta^{1}\ 
% x^{d}$, where $x$ is determined; indeed if $x$ is undetermined, the
% result holds trivially; by Corollary \ref{co:exh} either
% $\GG;(\O,x\oftp C);\D\vd M\hastype A$ or $(\GG,\O,\D);\cdot;x\oftp
% C;\vd M\hastype A$ and either $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ or
% $(\GG,\O,\D);\cdot;x\oftp C \vd M\hastype A$, depending on the
% polarity of $d$.  Thus $\GG\vd M\in \|E\ \Phi^{u}\Omega ^{0}\Delta
% ^{1}\ x^{d}\|$ or $\GG \vd M\in\|F\ \Phi^{u}\Omega ^{u}\Delta ^{u}\ 
% x^{-d}\|$ for some $d\in\{1,0\}$.

\enit 
\itc $\cD$ ends in $\mnot\_App^{1}$.
  Let $M$ be a ground term $g\ \Mm$ where $g\in\Sigma\cup\GG,
  g\not\equiv h$.  Then clearly $\GG\vd g\ \Mm\in \|g\ (Z_{1}
  \GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\| $,
%  where $\GG \prv \mnot(h\ 
% \ol{N_n^{1}}) = g\ (Z_{1} \GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\| $,
hence the claim by weakening.

\itc$\cD$ ends in $\mnot\_App^{2}$.
\btab
$\GG\vd\mnot(N_{i}) \blip  Q$ for some $1\leq i\leq n$ \bs
$\GG\vd h\ \ol{N_n^{1}}\hastype a$ \` By assumption\\
$\GG\vd N_{i}\hastype A_{i}$\`  By inversion \\
$\GG \prv M_{i}\in \| N_{i} \| \hastype A_{i}$ or $ \GG \prv M_{i}\in \| Q\| \hastype
 A_i$  \bi 
\etab
\bit
\item[Subcase]
\btab
$\GG \prv M_{i}\in \| N_{i} \| \hastype A_{i}$\ba
$\GG \prv h\ \ol{M_n^1}\in \| h\ \ol{N_n^1} \| \hastype a$\`  by rule $grApp$ \\
hence the claim by weakening
\etab
\item[Subcase]
\btab
$ \GG \prv M_{i}\in \| Q\| \hastype A_i$ \ba
 $\GG\vd M_{j}\in\|(Z_{j}\GG^{u}
 )^{1}\|$ for some $j\neq i, 1\leq j\leq n$\` By rule $grFlx$\\ $\GG \prv
 h\ \ol{M_n^1}\in \| h\ (Z_{1}\GG^{u} )^{1}\dots (Z_{i-1}\GG^{u}
 )^{1}\ N^{1}\ (Z_{i+1}\GG^{u} )^{1}\dots (Z_{m}\GG^{u} )^{1} \|
 \hastype a$ \` by rule $grApp$ \\ hence the claim by weakening. 
\etab
\enit
\itc $\cD$ ends in $\mnot\_Lam$. 
 \btab
$\GG,x\oftp A\vd\mnot(N)\blip Q$\bs
$\GG,x\oftp A \prv M\in \| N \|
\hastype B$ or $ \GG \prv M\in \| Q\| \hastype B$\bi
\etab
\bit
\item[Subcase]
\btab
$ \GG \prv M\in \| N\| \hastype B$\ba
$\GG \prv \lxua M\in \|\lxua N
\| \hastype A\TImp B$ \` by rule $grLam$ \\
hence the claim by weakening
\etab
\item[Subcase]
\btab
$ \GG \prv M\in \| Q\| \hastype B$\ba
 $ \GG \prv \lxua M\in \| \lxua Q\| \hastype
A\TImp B$\` by rule\\
% Q\| \hastype A\TImp B$\` 
hence the claim by weakening.  \etab\enit \enit
\end{proof}