\bit
\nitc for $\IP$ ends in $\imm\top$.
\nitc for $\IP$ ends in $\imm\perp$,  since by the restriction to complementable
 clauses, $\perp$ cannot occur as an assumption.
\itc
$$\IP=\ibnc{\ga\sp\s\vnx\eqd\Mn}{\ga\sp\s H}{\ga\sp \Pi(q\ \vnx\If H) \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnotd (\Pi(q\ \vS\If G))\imm\neg q \ \Mn$.
\btab 
$\ga\sp\s\vnx\eqd\Mn$\bs
$\ga\sp \ex\eqd M_i$ $(*)$ for some $1\leq i\leq n$\bs
$\gna\sn \BAnd_{\vT\in\cdot\vd\mnot(\vS)}\Pi( \neg q\ \vT\If \top )\And
\Pi(\neg q\ \vS\If \mnotg(G))\imm\neg q\
      \Mn$\` By rule $\mnotd\Imp$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \BAnd_{\vT\in\cdot\vd\mnot(\vS)}\Pi( \neg q\ \vT\If\top )\imm q\ \Mn$
\bv
$\gna\sn \Pi( \neg q\ \vT\If\top )\imm q\ \Mn$ for some $\vT\in\cdot\vd\mnot(\vS)$ \bv
$\gna\sn[\theta](\neg q\ \vT\If \top) \imm \neg q\ \Mn$   for some $\theta$\bv
$\gna\sn[\theta]\vT\eqd\Mn$\bv
$\gna\sn [\theta] T_i\eqd M_i$ \bv
$\perp$\`  $(*)$  and Lemma \ref{le:rigid} on above line
\etab
\item[\subcase]
\btab
$\gna\sn \Pi(\neg q\ \vS\If \mnotg(G))\imm\neg q\ \Mn$ \bv
$\gna\sn[\theta']\vS\eqd\Mn$\bv
$\gna\sn [\theta'] S_i\eqd M_i$\bv % for some $1\leq i\leq n$\bv
$\perp$\` From  line $(*)$ and  $S_i$ rigid.
\etab
\enit
\nitc $\IP$ ends in $\imm\Imp$, $\IM$ ends in $\imm\perp$: if $\top_q$ is the
only definition for $q$, then by schema satisfaction $\Pi(q\ \vnx\If H)$ could not be an assumption.
\nitc $\IP$ ends in $\imm\Imp$, $\IM$ ends in $\imm\perp$: ditto.
\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\mnotd(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.2$
\etab
\itc%And 2
$$\IP= \ianc{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And_2}$$
and $\IM$ ends in $\ga\vd\mnotd(D')\imm\neg Q$:
Symmetric to the above.
\itc
$$\IM= \ianc{\ga\sp \mnotd(D'_{1})\imm \neg Q}{\ga\sp\mnotd (D'_{1}\tensor
  D'_{2})\imm\neg Q}{\imm\And_1}$$
and $\IM$ ends in $\ga\vd D\imm Q$. By IH $2.3$
\itc
$$\IM= \ianc{\ga\sp \mnotd(D'_{2})\imm\neg  Q}{\ga\sp\mnotd (D'_{1}\tensor
  D'_{2})\imm\neg Q}{\imm\And_2}$$
and $\IM$ ends in $\ga\vd D\imm Q$. By IH $2.3$.
\itc
$$\IM= \ibnc{\ga\sp \mnotd(D'_{1})\imm\neg Q}{\ga\sp \mnotd(D'_{2})\imm
  \neg Q}{\ga\sp \mnotd(D'_{1}\And D'_{2})\imm\neg Q}{\imm\tensor}$$
and $\IM$ ends in $\ga\vd D\imm Q$. By IH $2.3$.

\enit