proposition: Lemma KS_thm_2_4_lemma3_0 : forall i alpha n, nf alpha -> const_pathS i (T1.cons alpha (S n) zero) (T1.cons alpha n zero).
proof: Proof. intros i alpha n H; destruct (zero_limit_succ_dec H). - destruct s. + subst. left. split; [discriminate | reflexivity]. + right with (canon (T1.cons alpha (S n) zero) (S i)). * split; [discriminate | reflexivity]. * rewrite canonS_lim2;auto. eapply KS_thm_2_4_lemma1; auto. -- apply cons_nf; auto. ++ apply canon_lt; auto. intro; subst; discriminate. ++ apply single_nf; apply nf_canon; auto. -- discriminate. -- apply KS_thm_2_4_lemma2. ++ apply single_nf. apply nf_canon; auto. ++ discriminate. - destruct s as [beta [Hbeta e]]; subst. right with (canon (T1.cons (T1.succ beta) (S n) zero) (S i)). + split; [discriminate | reflexivity]. + rewrite canonS_cons_succ_eqn2;auto. eapply KS_thm_2_4_lemma1; auto. * apply cons_nf; auto. apply lt_succ; auto. * discriminate. * apply KS_thm_2_4_lemma2; auto with T1. discriminate. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)