proposition: Lemma KS_thm_2_4_lemma1 : forall i alpha n beta beta', nf (T1.cons alpha n beta) -> beta <> zero -> const_pathS i beta beta' -> const_pathS i (T1.cons alpha n beta) (T1.cons alpha n beta').
proof: Proof. induction 3. - destruct H1; subst; left; now rewrite canon_tail. - destruct H1; subst; destruct (T1_eq_dec (canon x (S i)) zero). { rewrite e in *; destruct (const_pathS_zero H2). } { constructor 2 with (T1.cons alpha n (canon x (S i))). - now rewrite canon_tail. - apply IHclos_trans_1n; auto. + apply nf_LT_right with x;auto. apply canonS_LT; trivial. eapply nf_inv2, H. } Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)