proposition: Lemma KS_thm_2_4_lemma5 : forall i alpha beta, const_pathS i alpha beta -> nf alpha -> alpha <> zero -> const_pathS i (T1.phi0 alpha) (T1.phi0 beta).
proof: Proof. induction 1. { destruct H as [H e]; subst y; intros. destruct (zero_limit_succ_dec H0). - destruct s. + subst x; now destruct H1. + left; now rewrite canonS_lim1. - destruct s as [beta [H2 e]]; subst. rewrite canon_succ; auto. * now apply KS_thm_2_4_lemma4. } { destruct H as [H e];subst y; intros. destruct (zero_limit_succ_dec H1). - destruct s. + subst x; now destruct H2. + right with (T1.phi0 (canon x (S i))). * rewrite canonS_lim1; auto. split;[discriminate | trivial]. * apply IHclos_trans_1n. apply nf_canon;auto. apply T1limit_canonS_not_zero; auto. - destruct s as [beta [H3 e]]; subst x. destruct (T1_eq_dec beta zero). { subst beta; destruct (const_pathS_zero H0). } rewrite canon_succ in IHclos_trans_1n; auto. apply const_pathS_trans with (T1.phi0 beta); auto. + apply KS_thm_2_4_lemma4; auto. + rewrite <- const_pathSE. auto. } Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)