nt identifies the sub-steps arising
from the expansions, e.g.,  66 -> <23,4> means that step 66 in the new
proof corresponds to the 4th substep in expanding step 23 of the old proof.

Clauses in the new proof that match clauses in the old proof retain
the IDs from the old proof, and there is no entry in the map for them.
<A NAME="greatest_id_in_proof"></A><HR><PRE><B>int greatest_id_in_proof(Plist proof);
</B></PRE><A NAME="proof_id_to_clause"></A><HR><PRE><B>Topform proof_id_to_clause(Plist proof, int id);