proposition: Lemma reachable_through_general_ind: forall (P: V -> Prop), (forall x y, edge G x y -> P x -> P y) -> forall S y, reachable_through_set G S y -> Forall P S -> P y.
proof: Proof. intros. destruct H0 as [x [? ?]]. rewrite Forall_forall in H1. specialize (H1 _ H0). eapply reachable_general_ind; eauto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.find_not_in CertiGraph.graph.path_lemmas