proposition: Lemma valid_path_edge: forall (g: Gph) v e p, valid_path g (v, e :: p) -> g |= v ~> (dst g e).
proof: Proof. intros. destruct H. assert (strong_evalid g e) by (simpl in H0; destruct p; intuition). destruct H1 as [? [? ?]]. hnf. subst v. do 2 (split; auto). rewrite step_spec. exists e. 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