proposition: Lemma cons_standard_pathS : forall alpha n beta , nf (T1.cons alpha n beta) -> forall gamma i j, standard_pathS i beta j gamma -> gamma <> 0 -> standard_pathS i (T1.cons alpha n beta) j (T1.cons alpha n gamma).
proof: Proof. unfold standard_pathS; induction 2. - left; auto. + discriminate. + rewrite canon_tail. * now rewrite H1. * assumption. * intro; subst; simpl in H3; now destruct H3. - right; rewrite canon_tail; auto. + apply IHstandard_path_toS; auto. eapply nf_LT_right; auto. * eapply H. * apply canonS_LT; trivial. eauto with T1. intro; subst; simpl in H0; destruct H1. apply standard_path_toS_zero in H0; now destruct H0. + intro;subst; simpl in H0; apply standard_path_toS_zero in H0;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)