proposition: Lemma KS_thm_2_4_lemma1' : forall i alpha n beta , nf alpha -> alpha <> zero -> const_pathS i (T1.phi0 alpha) beta -> const_pathS i (T1.cons alpha (S n) zero) (T1.cons alpha n beta).
proof: Proof. Proof with auto with T1. intros i alpha n beta H H0 H1; destruct (zero_limit_succ_dec H). - destruct s. + now destruct H0. + destruct (const_pathS_first_step H1). { rewrite e; left; split. discriminate. rewrite canon_SSn_zero ; trivial. } { apply const_pathS_trans with (T1.cons alpha n (T1.phi0 (canon alpha (S i)))) ; trivial. { left; rewrite canon_SSn_zero ; eauto with T1. - split. + discriminate. + rewrite canonS_lim1 ; eauto with T1. } apply KS_thm_2_4_lemma1. - apply nf_cons_LT; trivial. apply canonS_LT ; eauto with T1. apply single_nf ; trivial. now apply nf_canon. - discriminate. - rewrite canon_lim1 in c ; eauto with T1. } - destruct s as [gamma [H2 H3]]; destruct (const_pathS_first_step H1). { rewrite e; left; subst alpha; repeat rewrite canonS_phi0_succ_eqn; trivial. now rewrite canonS_cons_succ_eqn2. } apply const_pathS_trans with (T1.cons alpha n (T1.cons gamma i zero)). left; subst alpha; rewrite canonS_cons_succ_eqn2 ; eauto with T1. split; [discriminate |]. reflexivity. apply KS_thm_2_4_lemma1 ; trivial. apply nf_cons_LT ; eauto with T1. + subst; apply LT_succ ; eauto with T1. + discriminate. + subst alpha. rewrite canonS_phi0_succ_eqn in c; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)