proposition: Lemma path_prop_merge: forall (g: Gph) p1 p2 P, paths_meet g p1 p2 -> path_prop g P p1 -> path_prop g P p2 -> path_prop g P (p1 +++ p2).
proof: Proof. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. unfold path_prop in *. unfold path_glue, fst, snd in *. destruct H0, H1. split; auto. apply Forall_app; easy. 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