proposition: Lemma phi_cases_aux : forall P : T2 -> Type, P zero -> (forall b1 b2, nf b1 -> nf b2 -> P [b1, b2]) -> (forall b1 b2 n, nf b1 -> nf b2 -> P (gcons b1 b2 0 (fin (S n)))) -> (forall b1 b2 n c, nf (gcons b1 b2 n c) -> omega t2<= c \/ (0 < n)%nat -> P (gcons b1 b2 n c)) -> forall alpha, nf alpha -> P alpha.
proof: Proof. Proof with auto with T2. intros until alpha; case alpha; auto with T2. destruct n;intros until t1;case (lt_ge_dec t1 omega). - intros l H ; assert (nf t1) by (inversion H ; auto with T2). case (lt_omega_inv H0 l); intro x;case x. + intro;subst t1; cbn. refine (X0 _ _ _ _). * inversion H ... * inversion H ... + intros;subst t1. apply X1; inversion H ... - intros;apply X2 ... - intros;apply X2 ... auto with arith. - intros;apply X2 ... 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)