proposition: Lemma copy_vvalid_weak_eq: forall (g1 g2: Graph) (g2'': Graph') (M: V -> Prop) x x0, ~ vvalid g1 x /\ ~ vvalid g2'' x0 \/ x0 = vmap g2 x -> copy M x g1 g2 g2'' -> Same_set (vvalid g2'') (reachable g2'' x0).
proof: Proof. intros. destruct H; [| subst x0; eapply copy_vvalid_eq; eauto]. destruct H0 as [COPY_si [COPY_gprv [COPY_gpre [COPY_vvalid [COPY_evalid [COPY_consi COPY_bij]]]]]]. rewrite COPY_vvalid. destruct H. assert (Same_set (reachable_by g1 x (Complement V M)) (Empty_set _)). 1: { rewrite Same_set_spec; intros v; rewrite Empty_set_spec. pose proof reachable_by_head_valid g1 x v (Complement V M); tauto. } assert (Same_set (reachable g2'' x0) (Empty_set _)). 1: { rewrite Same_set_spec; intros v; rewrite Empty_set_spec. pose proof reachable_head_valid g2'' x0 v; tauto. } rewrite H1, H2. apply image_Empty. 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