\begin{Lemma}
\label{le:disjD}
It is not the case that both $\GG;\O;(\D,x\oftp A)\vd M\hastype C$ and 
$(\GG,\O,\D);x\oftp A;\cdot\vd M\hastype C$.
\end{Lemma}
\begin{proof}
By simultaneous induction on the structure of $\cD::\GG;\O;(\D,x\oftp 
A)\vd M\hastype C$ and $\cD'::(\GG,\O,\D);x\oftp A;\cdot\vd M\hastype C$.
\end{proof}

\begin{Lemma}
\label{le:disjO}
It is not the case that both $\GG;(\O,x\oftp A);\D\vd M\hastype C$ and 
$(\GG,\O,\D);\cdot;x\oftp A\vd M\hastype C$.
\end{Lemma}
\begin{proof}
By simultaneous induction on the structure of $\cD::\GG;(\O,x\oftp 
A);\D\vd M\hastype C$ and $\cD'::(\GG,\O,\D);\cdot;x\oftp A\vd 
M\hastype C$.
\end{proof}

\begin{proof}
\end{proof}

% \begin{proof}
% First observe that $E\ \ol{x_{n}^{l}}$ can be re-written as $E\ 
% \GG^{u}\Omega'^{0}\Delta'^{1}\ x^{d}$, where $x\in\Omega$ or $x\in 
% \Delta$ and accordingly $\Delta'=\D$ or $\O'=\O$, depending on the 
% polarity of $x^{d}$; indeed if $x$ is undetermined, the result holds 
% trivially.  Assume $\god\vd M\in \|E\ \GG^{u}\Omega'^{0}\Delta'^{1}\ 
% x^{d}\|$ and $\god \vd M\in\|F\ \GG^{u}\Omega'^{u}\Delta'^{u}\ 
% x^{\mnot(d)}\|$ for some $d\in\{1,0\}$ Then it holds that both 
% $\Gamma;\Omega;(\Delta', x\oftp A) \vd M \hastype C$ or 
% $\Gamma;(\Omega', x\oftp A);\Delta \vd M \hastype C$ and 
% $\Gamma;(\Omega', x\oftp A);\Delta\vd M\hastype C$ or $\Gamma 
% ;\Omega;(\Delta', x\oftp A)\vd M\hastype C$.  Both cases are 
% impossible by uniqueness of strict contexts (Theorem 
% \ref{thm:uniqueD}).
% \end{proof}
