proposition: Theorem phi_cases' : forall a b, nf b -> {b1 :T2 & {b2:T2 | b = [b1, b2] /\ a t2< b1 /\ phi a b = b}} + {phi a b = [a, b]} + {b1 :T2 & {b2:T2 & {n: nat | b = gcons b1 b2 0 (fin (S n)) /\ a t2< b1 /\ phi a b = [a, (gcons b1 b2 0 (fin n))]}}}.
proof: Proof. Proof with auto with T2. intros a b Hb; pattern b; apply phi_cases_aux; trivial. - left;right; cbn ... - intros; case_eq (compare a b1); auto. + left;right; unfold phi; cbn; rewrite H1 ... + left;left; exists b1;exists b2; split ... split;simpl ... rewrite H1 ... + left;right; cbn; rewrite H1 ... - intros; case_eq (compare a b1). + left;right; cbn; rewrite H1 ... + right; exists b1, b2, n; repeat split ... cbn; rewrite H1 ... + left;right; cbn; rewrite H1 ... - intros; left;right; cbn; case_eq n; trivial. + intro; subst n; case_eq 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 ... inversion 1. 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)