proposition: Lemma phi_psi : forall beta gamma n, nf gamma -> limit_plus_fin beta n gamma -> phi alpha beta = beta -> [alpha, gamma] = phi alpha (succ gamma).
proof: Proof. intros; case (phi_fix _ H1). intros beta1 (beta2,(H2,H3)). assert (gamma = (gcons beta1 beta2 0 (fin n))). { subst beta. inversion H0. inversion H9. auto with T2. inversion H10. auto with T2. inversion H10;auto with T2. } subst gamma. cbn; subst beta; generalize H3 H1. case beta1;case beta2. - inversion 1. - inversion 2. inversion H2. - replace (succ (fin n)) with (fin (S n)). + intros;rewrite phi_to_psi_1; auto with T2. + induction n;cbn;auto with T2. - replace (succ (fin n)) with (fin (S n)). intros;rewrite phi_to_psi_1; auto with T2. induction n;cbn;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)