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. Proof with auto with T2. intros a b Hb; pattern b;apply phi_cases_aux. - left;right; cbn ... - intros; generalize (phi_of_psi a b1 b2); case (lt_ge_dec a b1). + left;left ... + left;right ... - intros; generalize (phi_of_psi_succ a b1 b2 n); case (lt_ge_dec a b1). + right; exists (gcons b1 b2 0 (fin n)); split. case n. * cbn; constructor ... * cbn; repeat constructor ... apply le_lt_trans with a ... * split ... cbn; generalize l;case b1. -- inversion 1. -- case n; cbn ... + left;right ... - left;right;cbn; case_eq n ... + intro;subst n; case_eq c. * intro; subst c; case H0;intro H1. -- inversion H1. ++ discriminate. ++ lt_clean. -- lt_clean. * intro t; case t ... -- intro t0;case t0 ... ++ intros n t1 e; subst c. case H0. ** destruct 1. discriminate H1. inversion H1; lt_clean ... ** inversion 1. - auto with T2. 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)