proposition: Lemma Lemma2_6_1 (alpha : T1) : nf alpha -> forall beta, beta t1< alpha -> {n:nat | const_path (S n) alpha beta}.
proof: Proof. transfinite_induction alpha. intros x H Hx; destruct (zero_limit_succ_dec Hx). - destruct s. + subst; intros. destruct (not_LT_zero H0). + intros beta H0; destruct (canonS_limit_strong Hx i H0) as [n1 H1]. assert (canon x (S n1) t1< x)%t1. { apply canonS_LT; auto. intro; subst; discriminate. } assert (nf (canon x (S n1))). { eapply nf_canon;eauto. } destruct (H (canon x (S n1)) H2 H3 beta) as [n2 Hn2]. * auto. * exists (Nat.max n1 n2); red;red; rewrite <- clos_trans_t1n_iff. constructor 2 with (canon x (S n1)). -- rewrite clos_trans_t1n_iff. apply Cor12_1 with n1; auto. auto with arith. left. split. ++ intro e;subst. destruct (@T1limit_not_zero zero) ; auto. ++ reflexivity. -- rewrite clos_trans_t1n_iff; apply Cor12_1 with n2; auto. auto with arith. - intros beta H0. destruct s as [x0 [H1 H2]]. subst. assert (Hx0: (x0 t1< T1.succ x0)%t1) by (apply LT_succ ;auto). assert ({beta t1< x0} + { beta = x0})%t1. { apply LT_succ_LT_eq_dec in H0; trivial. eauto with T1. } destruct H2. + destruct (H x0 Hx0 H1 beta l) as [n Hn]; exists n. right with x0. * rewrite canon_succ. -- split. ++ apply succ_not_zero. ++ auto. -- assumption. * assumption. + exists 1; subst;left. rewrite canon_succ; trivial. * split; trivial. -- now apply succ_not_zero. Defined.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)