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