proposition: Theorem phi_cases' : forall a b, nf b -> {b1 :T2 & {b2:T2 | b = [b1, b2] /\ a < b1 /\ phi a b = b}} + {phi a b = [a, b]} + {b1 :T2 & {b2:T2 & {n: nat | b = cons b1 b2 0 (finite (S n))/\ a < b1 /\ phi a b = [a, (cons b1 b2 0 (finite n))]}}}.
proof: Proof. intros a b Hb. pattern b; apply phi_cases_aux. left;right;simpl;auto with T2. intros. caseEq (compare a b1). left;right. unfold phi. simpl. rewrite H1;auto with T2. left. left. exists b1;exists b2; split. auto with T2. split;simpl;auto with T2. rewrite H1;auto with T2. left;right. simpl. rewrite H1;auto with T2. intros. caseEq (compare a b1). left;right. simpl. rewrite H1. auto with T2. right. exists b1;exists b2; exists n. repeat split;auto with T2. simpl. rewrite H1;auto with T2. left;right. simpl. rewrite H1;auto with T2. intros. left;right. simpl. caseEq n. intro; subst n. caseEq c. intro; subst c. case H0. destruct 1. discriminate H1. inversion H1. inversion 1. intro t;case t. intro t0;case t0. intros until t1;case t1. intro; subst c. case H0. 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. 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