proposition: Lemma vcopy1_copied_root_valid: forall (G G1: Graph) (G1': Graph') x x0, vcopy1 x G G1 G1' -> x0 = vmap G1 x -> vvalid G1' x0.
proof: Proof. intros. destruct H as [? [? [? ?]]]. subst. simpl. 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