proposition: Lemma path_to_appR : forall u gamma alpha, path_to gamma u alpha -> forall s t, s <> nil -> t <> nil -> u = s ++ t -> ~ In 0 u -> exists beta, path_to beta s alpha /\ path_to gamma t beta.
proof: Proof. intros u gamma alpha H s t H0 H1 H2 H3; rewrite path_to_path_toS_iff in H; [| trivial]. - destruct (@path_toS_appR (unshift u) gamma alpha H (unshift s) (unshift t)). + apply unshift_not_nil; auto. * intro; apply H3; subst. apply in_or_app; auto. + apply unshift_not_nil; intro; apply H3; subst. apply in_or_app; auto. now destruct H1. + subst; now rewrite unshift_app. + exists x;destruct H4; split. * rewrite path_to_path_toS_iff; auto. intro; apply H3; subst; apply in_or_app; auto. * rewrite path_to_path_toS_iff; auto. intro; apply H3; subst; apply in_or_app; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)