proposition: Lemma path_toS_decompose gamma s alpha : forall beta t u, s = t++u -> path_toS beta t alpha -> path_toS gamma u beta -> path_toS gamma s alpha.
proof: Proof. intros. rewrite H; eapply path_toS_app; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)