proposition: Lemma horpo_algebraic_left : forall M N, M >> N -> algebraic M.
proof: Proof. intros. destruct H. hyp. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)