proposition: Lemma ml_psi : forall beta0 beta n, moser_lepper beta0 beta n -> {t1 : T2 & {t2: T2| beta0 = [t1,t2] /\ alpha < 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: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo