proposition: Lemma closed_edge_closed_reachable: forall l, (forall x y, In x l -> edge G x y -> In y l) -> (forall x y, In x l -> reachable G x y -> In y l).
proof: Proof. intros. rewrite reachable_ind_reachable in H1. induction H1. + auto. + apply IHreachable. apply H with x; 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