proposition: Lemma beta_imp_horpo : forall M N, algebraic M -> M -b-> N -> M >> N.
proof: Proof. intros. constructor; try hyp. apply subject_reduction. hyp. apply beta_env_preserving. hyp. apply beta_algebraic_preserving with M; hyp. apply HBeta. hyp. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)