proposition: Lemma algebraic_lower : forall M Me, algebraic M -> algebraic (lower M Me).
proof: Proof. intros. rewrite <- (terms_lower_conv M Me); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)