$$\IP=\ibnc{\ga\sp\vnx\eqd\Mn}{\ga\sp G}{\ga\sp q\ \vnx\If G \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnota (q\ \ol{N^y_i}\If H)\imm\neg q \
\Mn$.
\btab
$\ga\sp\vnx\eqd\Mn$\bs
$\ga\sp N_j\eqd M_j$ $(+)$ and \\
$\ga\sp x\eqd M_i$ $(*)$ $1\leq i,j\leq n, i\not= j$\bv
$\gna\sn\mnota (q\ \ol{N^y_i})\And(\neg q\ \ol{N^y_i}\If
\mnotg(H))\imm\neg q \ \Mn$\` By inv. on $\mnota\Imp$
\etab
\bit
\item[Subcase]
\btab
$\gna\sn\mnota (q\ \ol{N^y_i})\imm\neg q \ \Mn$\bv
\etab
\bit
\item[$x\equiv y$]
\btab
$\gna\sn\mnota (q\ \ol{N^x_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_x}\If N_j\neqd Z_j)\imm\neg  q\ \vM$\\\bv
$\ga\sn[N_j/Z_j]Z_j\neqd M_j$\bv
$\perp$\` Above line and $(+)$
\etab
\item[$x\not\equiv y$]
\btab
$\gna\sn\mnota (q\ \ol{N^y_i}\If \top)\imm\neg q \ \Mn$\bv
$\gna\sn\mnot^i_i (q\ \ol{N^y_i}\If \top)\imm\neg q \ \Mn$\` By def.\\
$\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_y}\If N_j\neqd Z_j)\imm\neg  q\ \vM$\\\bv
$\ga\sn y\eqd M_i$\bv
$\perp$\` Above line, $(*)$ and eigenvariable cond.
\etab
\item[Subcase]
\btab
$(\neg q\ \ol{N^y_i}\If \mnotg(H))\imm\neg q \ \Mn$\` Analogous to
previous subcase
\etab
\enit
