\begin{proof}
We give a proof by induction  (course-of-value and structural) on the 
lexicographically ordered pair $\la S(p),M\ra$  over $\Sigma$:

\bit
\item
 Base for $S(p)$: $p$ is defined at stratum 1: we show 
 $\GG^{+}\prv p\ M$ or $\GG^{-}\prv \neg p\ M$ by induction over $M$: 
 first observe that $p$ and $\neg p$ can depend only on its recursive 
 call for n-ary constructors:

 \bit
\item
Base for $M$: projection from $\xn$:
\ben
\item
 consider $p\ (\l\xn.x_{i})$; if $p\ (\l\xn.x_{i})\not\in 
 heads(def(p))$, then there is a clause in $def(p)$ of the form $\neg 
 p\ (\l\xn.x_{i})$.  Thus $1.$ holds trivially.  Otherwise $p\ 
 (\l\xn.x_{i})$ must match a fact, since $p$ cannot depend neither on 
 itself or on other predicates.  Hence $p\ (\l\xn.x_{i})$ holds and 
 thus $1.$
\item
 Suppose $p\ (\l\xn.x_{i})\And\neg p\ (\l\xn.x_{i})$ hold: then 
 $(\l\xn.x_{i}) \cap Not(\l\xn.x_{i}) \not=\eset$; but this is 
 impossible by the Partition lemma \ref{lemma:part} hence $2.$.  
Simmetrically for $\neg p\ (\l\xn.x_{i})$ 

\noindent
 Analogously for a unary  constructor.  
\enen
\item
Step for $M$: $n$-ary constructor:
 \ben
 \item % Exh
 the induction hypothesis is (pushing in the universals):
\beq
( \BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) 
\And \BAnd \limits^q_{i = 1}\GG^{+} \Imp p\ (\l \xn.(E_i \  \xn\ 
z_{i}))) \Or\\
( \BOr \limits^m_{j = 1} \neg p\ (\l \xn .(Y_j \xn)) 
\Or \BOr \limits^q_{i = 1} \GG^{-} \Imp  \neg p\ (\l \xn.(E_i \  \xn\ 
z_{i})))
\eneq
By cases from IH:
\[
\begin{array}{ll}
\BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) \And 
\GG^{+} \Imp \BAnd \limits^q_{i = 1} p\ (\l \xn.(E_i \  \xn\ z_{i}))
& \mbox{first case}\\
p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) 
& \mbox{inversion on $m$}\\
\GG^{+}\Imp p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) \Or 
\GG^{-}\Imp\neg p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn))
& \mbox{weakening}
\\ \mbox{}\\
\BOr \limits^m_{j = 1} \neg p\ (\l \xn .(Y_j \xn)) 
\Or \BOr \limits^q_{i = 1} \GG^{-} \Imp  \neg p\ (\l \xn.(E_i \  \xn\ 
z_{i}))& \mbox{second case}\\
\neg p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)) 
& \mbox{inversion on $\neg m$}\\
\GG^{+}\Imp p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn))) \Or 
\GG^{-}\Imp\neg p\ (\l \xn . (a\ (\Ym \xn) \ (\Ep \xn)))
& \mbox{weakening}
\end{array}
\]

\item % Dsj
 the induction hypothesis is (pushing in the universals):
\beq
( \BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) 
\And \BAnd \limits^q_{i = 1}\GG^{+} \Imp p\ (\l \xn.(E_i \  \xn\ 
z_{i})) \And\\
 \BOr \limits^m_{j = 1} \neg p\ (\l \xn .(Y_j \xn)) 
\Or \BOr \limits^q_{i = 1} \GG^{-} \Imp  \neg p\ (\l \xn.(E_i \  \xn\ 
z_{i}))) \\
\Imp \bot\footnote{we use intuitionistic negation by 
falsehood to disinguish it here from the complement negation.}
\eneq

Again, suppose the negation of the thesis holds: but the result of applying 
inversion on both $m$ and $\neg m$ contradicts the IH.

\enen % end of 1.2. for S=1.

\enit

\item
Step for $S(p)$: suppose $p$ is defined at stratum $i$ and every 
predicate in $G$ is defined at stratum $j < i$:
\ben
\item %Exh
Proceed as above, with the difference that if $p\ (\l \xn .  (a\ (\Ym \xn) \ (\Ep \xn))$ 
matches a clause $p\ N \If G$, we may use the induction hypothesis on 
$G$, since every predicate in the latter is defined al a lower stratum 
or is a recursive call on a smaller term; Hence infer $ \GG^+ (G) \prv 
G$ or $\GG^{-}(G) \prv\neg G$ and thus the thesis
\item %Disj
Again, suppose the negation of the thesis holds: but the result of applying 
inversion on both $m$ and $\neg m$ contradicts the IH which applies 
to $G$ and $\neg G$ as well to the recursive calls.

\enen %end 1.2 sor S>1
\enit
\end{proof}


