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 (cons b1 b2 0 (finite (S n)))) -> (forall b1 b2 n c, nf (cons b1 b2 n c) -> omega <= c \/ (0 < n)%nat -> P (cons b1 b2 n c)) -> forall alpha, nf alpha -> P alpha.
proof: Proof. intros until alpha. case alpha. auto with T2. destruct n;intros until t1;case (lt_ge_dec t1 omega). intros. assert (nf t1). inversion H;auto with T2. case (lt_omega_inv H0 l). intro x;case x. intro;subst t1. simpl. refine (X0 _ _ _ _). inversion H;auto with T2. inversion H;auto with T2. intros;subst t1. apply X1. inversion H;auto with T2. inversion H;auto with T2. intros;apply X2. auto with T2. auto with T2. intros;apply X2. auto with T2. auto with arith T2. intros;apply X2. auto with T2. 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