proposition: Lemma si_reachable: forall (g1 g2: PreGraph V E) n, g1 ~=~ g2 -> Same_set (reachable g1 n) (reachable g2 n).
proof: Proof. intros. apply edge_equiv_reachable_equiv. + destruct H; auto. + intros; apply edge_si. 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