\itc $D=Q\If G$. Hence for all $\rho $ $\rho G\less \rho Q$ by termination.
By the first IH either $\SM \semic   \ga\sp \s G$ or $\foq\SP \semic \gna\fp\q
G$; moreover  for every ground $\vM_1,\vM_2$, it holds $\vM_1=\vM_2$ or
$ \vM_1\not=\vM_2$.
\ben
\item %1.
\btab
 $\SM \semic   \ga\sp \s G$\ba
$\ga\sp\s\vM_1\eqd \s\vM_2$\br $\vd\eqd$\\
$\ga\sp \s (q\ \vM_1)\If \s G\imm \s(q\ \vM_2)$\br $\imm\Imp$\\
$\ga\sp \s(q\ \vM_1\If G)\imm \s(q\ \vM_2)$\bsu\\
hence the thesis by weakening.
\etab
\item %2.
\btab
 $\SP \semic    \foq\gna\fp \q G$\ba
$\foq\ga\sp\q\vM_1\eqd \q\vM_2$\br $\vd\eqd$\\
$\foq\ga\fp\q\vM_1\neqd \q\vM_2$\br $\vd\neqd$\\
$\foq\gna\fp\q ( q\ \vM_1)\If \q G\imm  \q (q\ \vM_2)$\br\\
$\foq\gna\fp\q ( q\ \vM_1\If G)\imm  \q (q\ \vM_2)$\` By subst.\\
hence the thesis by weakening.
\etab
\item %3.
\btab
$\ga\sp \s G$\ba
$\foq\ga\fp\q\vM_1\eqd \q\vM_2$\br\\
$\foq\gna\fp \q (q\ \vM_1)\If \q G\imm \q( q\ \vM_2)$\br\\
$\foq\gna\fp \q( q\ \vM_1\If G)\imm \q( q\ \vM_2)$\bsu\\
hence the thesis by weakening.
\etab
\item %4 
\btab
$\foq\gna\fp \q G$\ba
$\foq\gna\fp\q\vM_1\eqd \q\vM_2$\br\\
$\foq\gna\fp \q (q\ \vM_1)\If \q G\imm \q( q\ \vM_2)$\br\\
$\foq\gna\fp \q( q\ \vM_1\If G)\imm \q( q\ \vM_2)$\bsu\\
hence the thesis by weakening.
\etab
\enen


Some examples will make the process clear. Consider the \texttt{cp} program on $\l$-terms:
\beq
cpapp &:& \PI{E_1,E_2,F_1,F_2}{exp}\\
& & cp\ (app\ E_{1}E_{2}) \ (app\ F_{1}F_{2})\\
&& \qquad\If  cp\ (E_{1}F_{1})\\ 
&& \qquad\If cp\ (E_{2}F_{2})\\
cplam &:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& & cp\ (lam\ E) \ (lam\ F)\\
& & \qquad\If \PI
{x}{ exp}\PI{y}{exp} cp\ (x\ y)\\
& & \qquad\qquad\Imp cp\ (E\ x) \ (F\ y)
\eneq
The augmentation procedure calls $x,y\oftp exp\vd^{\! cp\
  Ex\ Fy} \mnota( cp\ x\ y)$
%, glossing over the context $\Phi$ which
%is not active in this case. 
First\footnote{For brevity, we do not mention the target type \prop}
$cp\oftp exp\Imp\exp\vd \mnot^x_1(cp\ x\ y)= (\PI{E'}{exp} \neg cp\ E'\ y\If
x\neqd E')$, secondly $cp\oftp exp\Imp exp\vd
 \mnot^y_2(cp\ x\ y)= (\PI{F'}{exp} \neg cp\ x\ F'\If y\neqd F')$, yielding:
\beq
\ald(cplam)&:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& &  cp\ (lam\ E) \ (lam\ F)\If \\
& & \qquad \PI{x}{exp}\PI {y}{ exp}\\
& & \qquad (\PI{E'}{exp} \neg cp\ E'\ y\If x\neqd E')\And\\
& & \qquad (\PI{F'}{exp} \neg cp\ x\ F'\If y\neqd F')\Imp\\
&& \qquad\qquad
 cp\ (x\ y) \Imp cp\ (E\ x) \ (F\ y)
\eneq
while of course, $\ald(cpapp)=cpapp$, as enforced by $\alg \atm\top$. If
we had a one-parameter version of $cp$,  \ie
\beq
cplam' &:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& & cp'\ (lam\ E) \ (lam\ F)\If\\
& & \qquad \PI
{x}{ exp}  cp'\ (x\ x)\\
& & \qquad\qquad\Imp cp'\ (E\ x) \ (F\ x)
\eneq
Then we would get the  two calls to $cp\oftp exp\Imp exp\vd \mnot^x_1(cp'\ x\ x)= (\PI{E'}{exp} \neg cp'\ E'\ x\If
x\neqd E')$ and  $cp\oftp exp\Imp exp\vd
 \mnot^x_2(cp\ x\ x)= (\PI{F'}{exp} \neg cp'\ x\ F'\If
x\neqd F')$ and the augmented clause:
\beq
\ald(cplam')&:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& &  cp'\ (lam\ E) \ (lam\ F)\If \\
& & \qquad \PI{x}{exp}\\
& & \qquad (\PI{E'}{exp} \neg cp'\ E'\ x\If x\neqd E')\And\\
& & \qquad (\PI{F'}{exp} \neg cp'\ x\ F'\If x\neqd F')\Imp\\
&& \qquad\qquad
 cp'\ (x\ x) \Imp cp'\ (E\ x) \ (F\ x)
\eneq
Take the typing clause for lambda terms:
\beq
oflam &:&  \PI{E}{exp\Imp exp}\PI{T1,T2}{tp}\\
&& of\ lam(E) \ arrow(T1,T2)\If\\
& & \qquad \PI{x}{exp} of\ x\ T1 \Imp  of\ E\ x\,T2
\eneq
As $T1$ is an input term, the correspondent diseqution is inserted:
\beq
\ald(oflam) &:& \PI{E}{exp\Imp exp}\PI{T1,T2}{tp}\\
&& of\ lam(E) \ arrow(T1,T2)\If\\
& & \qquad \PI{x}{exp} of\ x\ T1 \Imp\\
& &\qqquad (\PI{T}{tp} \neg of\ x\ T\If T\neqd T1)\Imp\\
&&\qqquad\qquad  of\ (E\ x) \ T2.
\eneq

Consider now a predicate to perform instantiation of a binding
operator ( in the pattern fragment):
\beq
inlam & : & \PI {E}{exp\Imp exp} \PI {F} {exp} \\
& & inst\ (lam\ E) \ F \If\\
& &  \qquad\PI {x}{exp} (\PI {T}{exp} cp\ x\ T)\\
& & \qqquad  \Imp cp\ (E\ x)  \ F
\eneq
The call to $cp\oftp exp\Imp exp\vd\mnot^x_1 (\PI {T}{exp}
cp\ x\ T)$ yields the unsatisfiable clause $\PI{T}{exp}\PI{Z}{exp}
\neg cp\ x\ Z\If Z\neqd T$ and thus the augmentation is (ultimately) trivial.


Let us see how rule $\mnotxi\top$ enters the picture: consider the
\texttt{open} program
\beq
oplam &: & \PI{ E}{ exp\Imp exp} open\ (lam\ E)  \If\\
& & \qquad  \PI {x } {exp\Imp exp} open\ (E\
x)
\eneq
The judgment
$x\oftp exp;\top_{open}\vdf\alg( open\ Ex)$
triggers the rule $\mnotxi\top$,  thus $open\oftp exp\Imp\vd
\mnot^x_1(\top_{open})= \neg open\ x$:
\beq
\ald(oplam)&:&  \PI{ E}{ exp\Imp exp} open\ (lam\ E) \If  \\
& & \qquad \PI {x } {exp} \neg open\ x \Imp open\ (E\ x)
\eneq

Now consider $\Sigma = form,term\hastype type, all\hastype (term\Imp
form)\Imp form$ and the clause:
\beq
isdall & : & \PI{D}{form} isd\ (all\ D)\If \PI{x}{term} isd\ (D\ x)
\eneq
Here as $term\not\equiv form$, then $\ald(isdall)=isdall$.
