proposition: Lemma phi_le : forall alpha beta alpha' beta', nf beta -> phi alpha beta = [alpha', beta'] -> alpha <= alpha'.
proof: Proof. intros a b a' b' Hb;case (phi_cases a Hb). destruct 1. case (phi_fix _ e). intros x (beta2,(H,H0)). rewrite e. rewrite H. injection 1. intros; subst x; right;auto with T2. rewrite e;injection 1;left;auto with T2. intros (b0,(H1,(H2,H3))). rewrite H2; injection 1;left;auto with T2. 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