proposition: Theorem KS_thm_2_4 (lambda : T1) : nf lambda -> T1limit lambda -> forall i j, (i < j)%nat -> const_path 1 (canon lambda (S j)) (canon lambda (S i)).
proof: Proof. transfinite_induction lambda. clear lambda ; intros alpha Hrec Halpha H. destruct (zero_limit_succ_dec Halpha). - destruct s. + subst; discriminate. + destruct alpha. * discriminate. * nf_decomp Halpha. destruct (T1limit_cases Halpha H). { destruct a; subst alpha2. intros i0 j H1; destruct (@zero_limit_succ_dec alpha1) ; trivial. destruct s. { subst. now contradict H0. } { induction n. - repeat rewrite canonS_lim1; auto. apply KS_thm_2_4_lemma5. apply Hrec ; trivial. split ; trivial. split ; trivial. apply head_lt_cons ; trivial. apply nf_canon ; eauto with T1. apply T1limit_canonS_not_zero ; eauto with T1. - repeat rewrite canonS_lim2 ; eauto with T1. apply KS_thm_2_4_lemma1 ; trivial. apply cons_nf ; trivial. apply canon_lt ; trivial. apply single_nf. apply nf_canon ; eauto with T1. discriminate. apply KS_thm_2_4_lemma5 ; trivial. apply Hrec ; eauto with T1. split ; eauto with T1. apply nf_canon ; eauto with T1. apply T1limit_canonS_not_zero ; eauto with T1. } destruct s as [beta [H2 H3]]; subst; clear H i; induction n. { repeat rewrite canonS_phi0_succ_eqn ; eauto with T1. apply KS_thm_2_4_lemma3 ; eauto with T1. } { repeat rewrite canonS_cons_succ_eqn2 ; eauto with T1. apply KS_thm_2_4_lemma1 ; trivial. apply cons_nf ; trivial. apply lt_succ; auto. discriminate. apply KS_thm_2_4_lemma3 ; eauto with T1. } } intros i0 j H0; destruct a. repeat rewrite canon_tail ; eauto with T1. apply KS_thm_2_4_lemma1 ; trivial. apply nf_LT_right with alpha2 ; eauto with T1. apply canonS_LT ; eauto with T1. apply T1limit_canonS_not_zero ; eauto with T1. apply Hrec ; eauto with T1. split ; eauto with T1. split ; eauto with T1. apply tail_lt_cons; auto. all: intro; subst; discriminate. - destruct s as [beta [H0 H1]]; subst; destruct (@T1limit_succ beta); auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)