proposition: Lemma In_path_Subpath: forall g p1 p2 v, In_path g v p1 -> Subpath g p1 p2 -> In_path g v p2.
proof: Proof. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. unfold In_path in H. destruct H0. simpl in *. destruct H. + subst. auto. + right. destruct H as [e [? ?]]. 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