\ben % two sub-case
\item It is not the
  case that $\IP :: \ga\spp D \imm Q$ and $\IM :: \gna\sn \mnota(D)
  \imm \neg Q$. By mutual induction on the structure of $\IP$ and $\SP$.
\bit
  %\itc
%  $$\IP=\ianc{}{\ga\spp\perp_q\imm  Q}{\imm \atm}$$
%  But there can be no proof of $\neg Q$ from  $\mnota(\perp_q)=\top_q$.
\itc
$$\IP=\ibnc{\ga\sp\s\vN\eqd\Mn}{\ga\sp\s G}{\ga\sp \Pi(q\ \vN\If G) \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnota (\Pi(q\ \vN\If G))\imm\neg q \
\Mn$.
\btab
$\SP_1::\ga\sp\s G$\bs
$\ga\sp\s\vN\eqd\Mn$\bs
$\gna\sn\nn{ \vN}{\mnotg(G)}\imm\neg q \ \Mn$\\
\` By rule $\mnota\Imp$\\
$\ga\sp\s N_i\eqd M_i$ $(+)$ for all $1\leq i\leq n$\bv
$\GG\vd  M_i\in\|N_i\|$ $(*)$ for all  $1\leq i\leq n$\bv
\etab
\bit
\item[\subcase] $\s N_i\not\equiv\ex$, $\s N_i$ rigid:
\btab
$\ga\sn\mnotr(q\ \vN) \imm\neg q \ \Mn$\bv
$\ga\sn\BAnd_{1\leq i\leq n} \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\
[\ex/ Z_j] \Zn \imm\neg q \ \Mn$\bv
$\ga\sn \ex\eqd M_j$\bv
$\perp$ \` Above line and $(+)$.
\etab
\item[\subcase] $\s N_i\equiv\ex$:
\btab
$\ga\sn (\BAnd_{1\leq
           i\leq n,xR^{i}q}\mnotxi(q\ \vN))) \imm \s \neg q\
\Mn$ \bv %  $\imm\And_2$\\
$\ga\sn\mnotxi(\q \vN)\imm\neg q\ \Mn$\bv %\br $\mnotxi$\\
$\ga\sn\BAnd_{1\leq i\leq n}\BAnd_{N\in\GG\vd\mnot(M_i)}\Pi(\neg q\
\zij\If \top)\imm \neg q\ \Mn$ \bv
$\ga\sn\BAnd_{N\in\GG\vd\mnot(M_i)}\Pi(\neg q\ \zij\If \top)\imm \neg q\
\Mn$ \bv
$\gna\sn M_i\eqd[\theta] N$\bv
$\GG\vd M_i\in \|N\|$  for some $N\in\GG\vd\mnot( N_i)$\` By definition
of $\|\_\|$\\ 
$\perp$\` By term exclusivity (\ref{le:part}) with line $(*)$\\
% $\gna\sn\BAnd_{x\in \dom(\GG)}\BAnd_{\xrq}\mnotxi (q\
% \vN)\imm\neg q \ \Mn$\bv
% $\gna\sn\BAnd_{\xrq}\mnotxi (q\vN)\imm\neg q \ \Mn$\bv
% $\gna\sn\mnotxi (q\ \ol{N_{\ex}^i})\imm\neg q \ \Mn$\bv
% %$\gna\sn\mnotxi (q\ \ol{N^x_i})\imm\neg q \ \Mn$\` By rule $\mnota\Imp$\\
% $\gna\sn \BAnd_{1\leq j\leq n,j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%       \neg q\ \ol{Z^i_{\ex}}\If Z_j\neqd N_j)\imm\neg  q\ \vM$\bv
% $\gna\sn (\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ \ol{Z^i_{\ex}}\If
%       Z_j\neqd N_j)\imm\neg  q\ \vM$\bv 
% $\ga\sn[M_j/Z_j]Z_j\neqd N_j$\bv
%$\perp$\` Above line and $(+)$
\etab
\item[\subcase]
\btab
$\gna\sn\neg \Pi(q\ \vN\If\mnotg(G))\imm\neg q \ \Mn$\bv
$\gna\sn\mnotg(\s G)$\bv
$\perp$\bi $1$ on $\SP_1$
\etab
\enit
\itc $\IP$ ends in $\imm\tensor,\imm\And,\imm\Pi$: by IH $2.4.1$ similarly to
 case $2.1$ with $\mnota$ in place of $\mnotd$.
\enit
\item It is not the
  case that $\IP :: \ga\spp D \imm Q$ and $\IM :: \gna\sn \mnota(D')
  \imm \neg Q$. By simultaneous induction on the structure
  of $\IP$ and $\IM$:
% and mutual induction on the structure of $\SP$:
  \bit
  \nitc $\IP$ ends in $\imm\top$.
  \nitc $\IP$ ends in $\imm\perp$, by restriction to complementable clauses and schema satisfaction.
  \nitc $\IP$ ends in $\imm\Imp$, $\IM$ ends in $\imm\perp$, as above.
\newcommand{\vny}{\overline{N^y_i}}  
\itc
$$\IP=\ibnc{\ga\sp\s\vny\eqd\Mn}{\ga\sp\s G}{\ga\sp \Pi(q\ \vny\If G) \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnota (\Pi(q\ \vS\If G'))\imm\neg q \
\Mn$, from a different block.
\btab
$\SP_1::\ga\sp\s G$\bs
$\ga\sp\s\vny\eqd\Mn$\bs
$\gna\sn\nn{ \vS}{\mnotg(G')}\imm\neg q \ \Mn$\\
\` By rule $\mnota\Imp$, $y\not\equiv x$\\
$\ga\sp\s N_i\eqd M_i$ $(+)$ for all $1\leq i\leq n$\bv
\etab
\bit
\item[\subcase] $\s N_i\not\equiv e_y$, $\s N_i$ rigid:
\btab
$\ga\sn\mnotr(q\ \vS) \imm\neg q \ \Mn$\bv
$\ga\sn\BAnd_{1\leq i\leq n} \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\
[\ex/ Z_j] \Zn \imm\neg q \ \Mn$\bv
$\ga\sn \ex\eqd M_j$\bv
$\perp$ \` Above line, $N_j$ rigid and $(+)$.
\etab
\item[\subcase] $\s N_i\equiv e_y$:
\btab
$\perp$ \` Above line, eigenvariable condition and $(+)$.
\etab
\item[\subcase]
\btab
$\gna\sn\neg \Pi(q\ \vS\If\mnotg(G'))\imm\neg q \ \Mn$\bv
$\ga\sn[\sigma]\vS\eqd\Mn$\bv
$\perp$ \` Above line, eigenvariable condition and $(+)$.
\etab
  \enit
 \itc
$$\IP=\ibnc{\ga\sp\s\vN\eqd\Mn}{\ga\sp\s G}{\ga\sp \Pi(q\ \vN\If G) \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnota (\top_q))\imm\neg q \
\Mn$, from a different block.
\btab
$\SP_1::\ga\sp\s G$\bs
$\ga\sp\s\vN\eqd\Mn$\bs
$\gna\sn\BAnd_{x\in\dom(\GG)} (\BAnd_{1\leq
  i\leq n,xR^{i}q} \mnotr(\top_q)\imm\neg q \ \Mn$\\
\` By rule $\mnota\top$\\
$\ga\sp\s N_i\eqd M_i$ $(+)$ for all $1\leq i\leq n$\bv
$\GG\vd  M_i\in\|N_i\|$ $(*)$ for all  $1\leq i\leq n$\bv
 $\s N_i\not\equiv\ex$, $\s N_i$ rigid\\
$\ga\sn\mnotr(q\ \vN) \imm\neg q \ \Mn$\bv
$\ga\sn\BAnd_{1\leq i\leq n} \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\
[\ex/ Z_j] \Zn \imm\neg q \ \Mn$\bv
$\ga\sn \ex\eqd M_j$\bv
$\perp$ \` Above line and $(+)$.
\etab
\itc%And 1
$$\IP= \ianc{\ga\sp D_{1}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And_1}$$
and $\IM$ ends in $\ga\vd\mnota(D')\imm\neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
% $\gna\sn \mnota (D'_1)\tensor\mnota(D'_2)\imm\neg Q$\br $\mnota\And$\\
% $\gna\sn\mnota(D'_1)$\bv
$\perp$\bi $2.4.2$
\etab
\itc $\IP$ ends in $\imm\And_1,\imm\tensor$, $\IM$ ends in $\imm\And_i,\imm\tensor$: analogously by IH $2.4.2$.
  \enit
\enen %end two 2.4 subcases
