proposition: Lemma horpo_eq_compat : forall M M' N N', M = M' -> N = N' -> M >> N -> M' >> N'.
proof: Proof. intros; rewrite <- H, <- H0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)