proposition: Lemma in_path_or_cons: forall g v e p n, v = src g e -> (In_path g n (v, e :: p) <-> n = v \/ In_path g n (dst g e, p)).
proof: Proof. intros. subst. unfold In_path. simpl. intuition. + destruct H0 as [e0 [? ?]]. destruct H. 1: subst; intuition. right; right; exists e0. split; auto. + right. exists e. intuition. + right. destruct H as [? [? ?]]. exists x. intuition. 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