toCpfOrderingConstraintProof must handle non-singleton [UsableOrder MSL]

[jwaldmann]

several orders in sequence result in a proof tree with several nodes.

we alread compute intermediates for this.

intermediates
  :: Trs t t1 t2
     -> GroupedTrs Symbol Symbol Label
     -> [(Map MSL Bool, TerminationOrder MSL)]
     -> [TaggedGroupedTrs Symbol Symbol Label]

At the top of the proof tree, semLab. Then, for each (usableOrder, labelledtrs) <- zip usableorders (intermediates ...), a redPairProc node (with UR). Then, for the end of the list, an unlabel node. Below this, the continuation of the proof (the invisible argument of toCpfProof).

[abau]

fixed by https://github.com/apunktbau/co4/commit/9d5c7fcccf5229d78e9bd28507b2022b3ccf31cc