proposition: Lemma ml_psi : forall beta0 beta n, moser_lepper beta0 beta n -> {t1 : T2 & {t2: T2| beta0 = [t1,t2] /\ alpha t2< t1}}.
proof: Proof. intros beta0 beta n (H1,H2). case (phi_fix _ H2). intros x (y,(H3,H4)); exists x;exists y;auto. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)