We now prove the crucial exhaustivity lemmata.

\newcommand{\cu}{(\GG,\Omega,\Delta, x\oftp C);\cdot;\cdot}
\newcommand{\cxtr}{\GG;\cdot;  x\oftp C}
\newcommand{\cxto}{\GG; x\oftp C;\cdot}


\begin{lemma}
\label{le:exh1} Let $M$ be a simple pattern and $\cu\vd M\buda A$. 
Then:
\ben
\item
 $\cxtr\vd M\da A$ or $\cxto\vd M\da A$.
\item
 $\cxtr\vd M\bua A$ or $\cxto\vd M\bua A$.
\enen
\end{lemma}
\begin{proof}
By simultaneous induction on $\cD_{1}::\cu\vd M\da A$ and $\cD_{2}::\cu\vd M\bua A$.
 \bit
\itc 
$$\cD = \ianc{c\oftp A\in\Sigma}{\cu \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\cxto \prv  c\da A}{cIdc}$$
\itc
$$\cD = \ianc{}{(\GG,\Omega,\Delta,x\oftp C,y\oftp A);\cdot; \cdot  \prv  y\da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,\Omega,\Delta,y\oftp A);x\oftp C; \cdot  \prv  y\da 
A}{cId^{u}}$$
$$\cD = \ianc{}{\cu \prv  x\da C}{cId^{u}}$$
Then
$$\cE= \ianc{}{\cxtr \prv  x\da C}{cId^{1}}$$

\itc No case for $\cD = Id^{1}$.
\itc
$$\cD = \ianc{\cu\prv  M\da P}{\cu \prv  M\bua P} {cAt}$$
\btab
 $\cu\prv  M\da P$ \` By inversion\\ 
 $\cxtr \prv  M\da P$  \` By IH \\
 $\cxtr \prv  M\bua P$ \` By rule $cAt$\\
 $\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$ \` By weakening
 $\cxto \prv  M\da P$ \`  By IH \\
$\cxto \prv  M\bua P$ \` By rule $cAt$\\
 $\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$ \` By weakening
\etab
\itc
$$\cD = \ianc{(\GG,\Omega,\Delta,y\oftp A) \prv M\bua B}{\cu\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
\btab
$(\GG,\Omega,\Delta,y\oftp A) \prv M\bua B$ \` By inversion\\
$GG;\Omega;(\Delta,x\oftp C,y\oftp A)\vd M\bua $ \` By IH\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ \` By rule $c\TImp I$\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$ \` By weakening\\
$(GG,\Omega,\Delta,y\oftp A);x\oftp C;\cdot\vd M\bua $ \` By IH\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$ \` Similarly
\etab
\itc
$$\cD = \ibnc{\cu \vd M \da A \RImp B}{\cu \vd N \bua A}{\cu \vd
M\, N^1 \da B}{c\RImp E}$$
By inversion there are derivations $\cD_{1}:: \cu \vd M \da A \RImp 
B$ and $\cD_{2}:: \cu \vd N \bua A$.
There are four disjoint sub-cases, stemming from the IH  :
\ben
\item $\cxtr\vd M\da A\RImp B$ and $\cxtr\vd N\bua A$. Thus $\cxtr\vd M\ 
N^{1}\da B$, hence  by weakening the thesis.
\item $\cxto\vd M\da A\RImp B$ and $\cxto\vd N\bua A$. Thus $\cxto\vd M\ 
N^{1}\da B$, hence  by weakening the thesis.
\item $\cxtr\vd M\da A\RImp B$ and $\cxto\vd N\bua A$. Thus  $\cxtr\vd M\da A\RImp B$
or  $\cxto\vd M\da A\RImp B$ and $\cxtr\vd N\bua A$ or $\cxto\vd N\bua 
A$. Hence the thesis.
\item Symmetrical to the last one.
%
\enen
\enit
\end{proof}

