 Let $D\inn \defp(q,\cP)$: It is not the case that
$\IP :: \ga\spp  D \imm Q$ and
$\IM :: \gna\sn \mnotd(D) \imm \mnotg( Q)$.
By mutual induction on the structure of $\IP$ and $\SP$,
 by assuming their existence:
%\enen
% We proceed by mutual induction on the structure of $\IP$ and $\SP$,
% by assuming their existence.%  Note that immediately $\GG\vd\mnotg(Q)=\neg Q$. Moreover, a
% negative definition implies an atom iff so does every disjunct; thus
% it will suffice to show absurdity for one of the latter.
% The second statement thus unfolds in four distinct cases:
% \ben %start four cases
% \item[\fbox{2.1}] %first case
%  Let $D\inn \defp(q,\PP)$ . 
% It is not the case that:
% $\IP :: \ga\spp  D \imm Q$ and
% $\IM :: \gna\sn \mnotd(D)\imm \neg Q$.
\bit
\itc
$$\IP=\ianc{}{\ga\spp\perp_q\imm  Q}{\imm\perp}$$
But there can be no proof of $\neg Q$ from  $\mnotd(\perp_q)=\top_q$.
\itc
$$\IP=\ibnc{\ga\spp[\sigma]\vN\eqd \vM}{\ga\spp [\sigma]G}{\ga\spp \Pi(q\ \vN\If G)\imm q\ \vM}{\imm\Imp}$$
and
$\IM$ ends in $\gna\sn \mnotd (\Pi(q\ \vN\If G))\imm \neg q\
\vM$:
\btab
$\ga\spp[\sigma]\vN\eqd \vM$\bs
$\cdot\vd\vM\in\|\vN\|$ $(*)$\`By definition of \ of $\|\_\|$\\ 
$\SP_1::\ga\spp [\sigma]G$  \bs
% $\gna\sn (\neg q\ \vM_1\If \mnotg(G))\imm \neg q\ \vM_2$\bv
$\gna\sn \BAnd_{\vS\in\cdot\vd\mnot(\vN)}\Pi( \neg q\ \vS\If \top) \And  \Pi(\neg q\ \vN\If      \mnotg(G))\imm \neg q\ \vM$\` By rule $\mnotd\Imp$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \BAnd_{\vS\in\cdot\vd\mnot(\vN)}\Pi( \neg q\ \vS\If \top)\imm\neg q\
      \vM$\bv
$\gna\sn \Pi( \neg q\ \vS\If \top)\imm\neg q\
      \vM$ for some $\vS$ \bv
$\gna\sn[\theta](\neg q\ \vS)\If\top\imm \neg q\ \vM$  for some $\theta$\bv
$\gna\sn[\theta]\vS\eqd\vM$\bv
$\cdot\vd\vM\in\|\mnot (\vN)\|$\` By definition of $\| \_ \|$\\
$\perp$\` By term exclusivity with $(*)$
\etab
\item[\subcase]
\btab
$\gna\sn\Pi(\neg q\ \vN\If \mnotg(G))\imm \neg q\ \vM$\bv
$\gna\snp ([\sigma]G)$\bv
$\perp$\bi $1$ \wrt $\SP_1$
\etab
\enit%end At
\itc %imm\tensor
$$\IP= \ibnc{\ga\sp D_{1}\imm Q}{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\tensor
  D_{2})\imm Q}{\imm\tensor}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\tensor
  D_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\ga\spp  D_2\imm Q$\bs
$\gna\sn \mnotd (D_1)\And\mnotd (D_2)\imm\neg Q$\br $\mnotd\tensor$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \mnotd (D_1)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
\item[\subcase]
\btab
$\gna\sn \mnotd (D_2)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
\enit
\itc%And 1
$$\IP= \ianc{\ga\sp D_{1}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\And
  D_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\gna\sn \mnotd (D_1)\tensor\mnotd(D_2)\imm\neg Q$\br $\mnotd\And$\\
$\gna\sn\mnotd(D_1)$\bv
$\perp$\bi $2.1$
\etab
\itc%And 2
$$\IP= \ianc{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\And
  D_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_2\imm Q$ \bv
$\gna\sn \mnotd (D_1)\tensor\mnotd(D_2)\imm\neg Q$\br $\mnotd\And$\\
$\gna\sn \mnotd (D_2)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
% \itc %\Pi imm no more
% $$\IP= \ibnc{\GG\vd t\hastype A}{ \ga\spp [t/x] D \imm Q}{\ga\spp\PI
%  { x}{A}D \imm Q}{\imm\Pi}$$
% and $\IM$ ends in $\gna\sn\mnotd(\PI{x}{A}D)\imm\neg Q$:
% \btab
% $\ga\spp [t/x] D\imm Q$\bs
% $\gna\sn\mnotd([u/x]D)\imm\neg Q$\br $\mnotd\Pi$\\
% $\gna\sn \mnotd([t/u,u/x]D)\imm\neg Q$\` By substitution\\
% $\perp$\bi $2.1$
% \etab
\enit