proposition: Lemma horpo_algebraic_preserving : forall M N, algebraic M -> M >> N -> algebraic N.
proof: Proof. intros M N Mnorm MN. inversion MN. inversion H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)