proposition: Lemma edge_equiv_reachable_equiv: forall (g1 g2: PreGraph V E), (forall x, vvalid g1 x <-> vvalid g2 x) -> (forall x y, edge g1 x y <-> edge g2 x y) -> forall n, Same_set (reachable g1 n) (reachable g2 n).
proof: Proof. cut (forall (g1 g2 : PreGraph V E), (forall x, vvalid g1 x <-> vvalid g2 x) -> (forall x y, edge g1 x y <-> edge g2 x y) -> forall n, Included (reachable g1 n) (reachable g2 n)). 1: intros; split; intros; apply H; [auto | auto | symmetry; auto | symmetry; auto]. intros; intro; intros. unfold Ensembles.In in *. rewrite @reachable_ind_reachable in *. induction H1. + constructor. rewrite H in H1; auto. + rewrite H0 in H1. apply ind.reachable_cons with 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