proposition: Lemma edge_copy_vvalid_mono: forall (G1 G2: Graph) (G1' G2': Graph') g root M es_done e0 x0, edge_copy g root M (es_done, e0) (G1, G1') (G2, G2') -> vvalid G1' x0 -> vvalid G2' x0.
proof: Proof. intros. unfold edge_copy in H. destruct_relation_list GG0 in H; destruct GG0 as [G G']. eapply ecopy1_vvalid_mono; eauto. eapply extended_copy_vvalid_mono; eauto. 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