 for back_demod.
<A NAME="back_unit_deletion_just"></A><HR><PRE><B>Just back_unit_deletion_just(Topform c);
</B></PRE>This routine builds and returns a justification list for back_unit_deletion.
<A NAME="binary_res_just"></A><HR><PRE><B>Just binary_res_just(Topform c1, int n1, Topform c2, int n2);
</B></PRE>This routine builds and returns a justification list for binary resolution.
(Binary res justifications may also be constructed in resolve(), along
with hyper and UR.)
<A NAME="binary_res_just_by_id"></A>