proposition: Lemma horpo_beta_wf : forall M, algebraic M -> SN.SN horpo M.
proof: Proof. intros M Mnorm. apply SN.Acc_transp_SN. apply horpo_comp_imp_acc. assert (Mid_comp: CompH (subst (emptySubst_correct M))). apply subst_comp; trivial. red; contr. intros p T; destruct p; try_solve. rewrite <- (emptySubst_neutral (emptySubst_correct M)); trivial. apply emptySubst_empty. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)