proposition: Lemma phi_to_psi_2 : forall beta1 beta2 n, beta1 <= alpha -> [alpha, (cons beta1 beta2 0 (F n))] = phi alpha (cons beta1 beta2 0 (F n)).
proof: Proof. intros. case n. simpl (F 0). generalize (phi_of_psi alpha beta1 beta2). case (lt_ge_dec alpha beta1). intro; (absurd (alpha<alpha)). apply lt_irr. eapply lt_le_trans;eauto with T2. auto with T2. intro n0;generalize (phi_of_psi_succ alpha beta1 beta2 n0). case (lt_ge_dec alpha beta1). 2:auto with T2. intro; absurd (alpha < alpha). apply lt_irr. eapply lt_le_trans;eauto 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