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