proposition: Lemma phi_to_psi_6 : forall beta, nf beta -> phi alpha beta = beta -> [alpha, beta] = phi alpha (succ beta).
proof: Proof. intros; case (phi_fix _ H0 ). intros beta1 (beta2,(H2,H3)); subst beta. generalize (phi_to_psi_1 beta2 0 H3). simpl (succ (gcons beta1 beta2 0 zero)); generalize H3 ; case beta1. inversion 1. auto with T2. 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)