proposition: Lemma reachable_path_edge_in: forall (g: Gph) (p: path) (l y : V), g |= p is l ~o~> y satisfying (fun _ : V => True) -> forall e, In e (snd p) -> reachable g l (src g e) /\ reachable g l (dst g e).
proof: Proof. intros. split. - assert (In_path g (src g e) p) by (right; exists e; split; auto). eapply reachable_path_in; eauto. - assert (In_path g (dst g e) p) by (right; exists e; split; auto). eapply reachable_path_in; eauto. 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