proposition: Lemma path_prop_split: forall (g: Gph) p1 p2 P, paths_meet g p1 p2 -> valid_path g (p1 +++ p2) -> path_prop g P (p1 +++ p2) -> path_prop g P p1 /\ path_prop g P p2.
proof: Proof. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. unfold path_prop. red in H1. unfold path_glue, fst, snd in H0, H1 |-* . destruct H1. split; split; auto. - eapply Forall_incl; eauto. apply incl_appl, incl_refl. - rewrite Forall_forall in H2. red in H. destruct H as [n [? ?]]. destruct p1. + simpl in H, H3. subst. easy. + apply pfoot_in_cons in H. destruct H as [e' [? ?]]. simpl in H3. subst. apply H2. apply in_or_app. left. easy. - eapply Forall_incl; eauto. apply incl_appr, incl_refl. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec