proposition: Lemma reachable_by_subset_reachable: forall (g: Gph) n P, Included (reachable_by g n P) (reachable g n).
proof: Proof. repeat intro. unfold reachable. destruct H as [p [? [? ?]]]. exists p. split; trivial. split; trivial. apply path_prop_weaken with 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