\section{Definitions and Notation}
\label{defs}
We list some relevant notions. We assume 
familiarity with the following:
\bit
\item
Basic proof theory.
\item
Higher-order logic programming including  \ho unification.
\enit


%  \bedef [Linear] A term $u$ is {\em linear} if there is no multiple occurrence of the 
% same variable therein.  The term $\q t$ is called {\em restricted} 
% \wrt $t$ if either there is $x \in t$ such that $\q x$ is not linear 
% or there are two distinct variables $x_1,x_2 \in t$ such that $\q x_1$ 
% and $\q x_1$ share a variable.  \enef



We write $\vt$ for a tuple of elements, in this case terms, whose 
length is unimportant:
$\tn$ will be used as an abbreviation of $t_1 \mdots t_n$; $\tm = \sm$ (resp.\ $\tm 
\nq\sm$) will  
stand for 
\[\BAnd^m_{i=1} t_i = s_i  \quad \quad\quad\BOr^m_{i=1} t_i \nq s_i\]
 taking the place sometimes of the more cumbersome notation 
$\ol{\tm = \sm}$.
 We use $[N/x]M$ for the result of the capture-avoiding 
substitution of $N$ for $x$ in $M$.
For a syntactic object ${\cal O}$, $FV({\cal O})$ will denote the set 
of its free variables.







