proposition: Lemma si_reachable_direct: forall (g1 g2: PreGraph V E) x y, g1 ~=~ g2 -> (reachable g1 x y <-> reachable g2 x y).
proof: Proof. intros. apply (si_reachable _ _ x) in H. destruct H. split; intros. + apply (H y); auto. + apply (H0 y); 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