proposition: Lemma copy_vvalid_eq: forall (g1 g2: Graph) (g2'': Graph') (M: V -> Prop) x, copy M x g1 g2 g2'' -> Same_set (vvalid g2'') (reachable g2'' (vmap g2 x)).
proof: Proof. intros. destruct H as [COPY_si [COPY_gprv [COPY_gpre [COPY_vvalid [COPY_evalid [COPY_consi COPY_bij]]]]]]. rewrite Same_set_spec; intros v'. split; [intros | apply reachable_foot_valid]. rewrite (app_same_set COPY_vvalid) in H. rewrite image_set_spec in H. destruct H as [v [? ?]]; subst v'. apply (guarded_morphism_reachable COPY_bij); [rewrite (weak_edge_prop_si _ _ _ COPY_si); apply Included_refl |]. rewrite <- COPY_si. rewrite <- (reachable_by_idempotent _ _ _ _); auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism