proposition: Lemma horpo_RC : forall M N, M >>= N -> M >> N \/ M = N.
proof: Proof. intros; inversion H; fo. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)