proposition: Theorem phi_cases : forall a b, nf b -> {phi a b = b}+ {phi a b= [a, b]}+ {b': T2 | nf b' /\ phi a b = [a, b'] /\ succ b' = b}.
proof: Proof. intros a b Hb. pattern b;apply phi_cases_aux. left;right. simpl; auto with T2. intros. generalize (phi_of_psi a b1 b2). case (lt_ge_dec a b1). left;left;auto with T2. left;right;auto with T2. intros. generalize (phi_of_psi_succ a b1 b2 n). case (lt_ge_dec a b1). right. exists (cons b1 b2 0 (finite n)). split. case n. simpl;constructor;auto with T2. simpl. repeat constructor;auto with T2. apply le_lt_trans with a;auto with T2. split; auto with T2. simpl. generalize l;case b1. inversion 1. case n;simpl;auto with T2. left;right. auto with T2. left;right;simpl. caseEq n. intro;subst n. caseEq c. intro; subst c. case H0;intro. inversion H1. discriminate H2. lt_clean. lt_clean. intro t; case t. intro t0;case t0. intros n t1 e; subst c. case H0. unfold omega; destruct 1. discriminate H1. inversion H1; lt_clean;auto with T2. inversion 1. auto with T2. auto with T2. 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