proposition: Lemma path_toS_tail alpha s beta : path_toS beta s alpha -> forall gamma n, nf (T1.cons gamma n alpha) -> path_toS (T1.cons gamma n beta) s (T1.cons gamma n alpha).
proof: Proof. induction 1. - subst; left; split. + discriminate. + rewrite canon_tail; auto. * destruct H; now subst. * now destruct H. - intros; subst; right with (T1.cons gamma0 n (canon alpha (S i))). + split. * discriminate. * rewrite canon_tail; auto. now destruct H. + destruct H; subst; apply IHpath_toS; auto. eapply nf_LT_right; eauto. apply canonS_LT; trivial. eapply nf_inv2, H1. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)