lds and returns a justification list for a paramodulation
inference.  The position vectors are not copied.
<A NAME="para_just_rev_copy"></A><HR><PRE><B>Just para_just_rev_copy(Just_type rule,
			Topform from, Ilist from_vec,
			Topform into, Ilist into_vec);
</B></PRE>This routine builds and returns a justification list for a paramodulation
inference.  The position vectors are copied and reversed.
<A NAME="primary_just_type"></A><HR><PRE><B>BOOL primary_just_type(Topform c, Just_type t);
</B></PRE>Does a cl