proposition: Lemma edge_preserved_rev_foot0: forall (P: V -> Prop), (forall x y, reachable G x y -> P x -> P y) -> forall l y, reachable_through_set G l y -> ~ P y -> reachable_by_through_set G l (Complement _ P) y.
proof: Proof. intros. destruct H0 as [s [? ?]]; exists s; split; auto. apply edge_preserved_rev_foot; auto. 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