proposition: Lemma reachable_path_in': forall (g: Gph) (p: path) (l y : V), g |= p is l ~o~> y satisfying (fun _ : V => True) -> forall z, In_path g z p -> reachable g z y.
proof: Proof. intros. apply reachable_by_path_split_in with (n := z) in H; auto. destruct H as [p1 [p2 [? [? ?]]]]. exists p2. apply H2. 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