proposition: Lemma In_path_glue: forall g p1 p2 v, In_path g v (p1 +++ p2) -> In_path g v p1 \/ In_path g v p2.
proof: Proof. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. unfold path_glue in H. simpl in H. unfold In_path in *. simpl in *. destruct H. 1: left; left; auto. destruct H as [e [? ?]]. rewrite in_app_iff in H. destruct H; [left | right]; right; exists e; split; auto. 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