proposition: Lemma valid_path_cons_iff: forall g v e p, valid_path g (v, e :: p) <-> v = src g e /\ strong_evalid g e /\ valid_path g (dst g e, p).
proof: Proof. intros. split; intros. + pose proof (valid_path_cons _ _ _ _ H). destruct H. subst v. do 2 (split; auto). simpl in H1. destruct p; intuition. + destruct H as [? [? ?]]. simpl in *. split; auto. destruct p; 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