fact: Definition vcopy1 root (g1 g2: Graph) (g2': Graph') := let PV_root := eq root in let PE_root := Intersection _ (weak_edge_prop PV_root g1) (evalid g1) in g1 ~=~ g2 /\ guarded_pointwise_relation (Complement _ PV_root) eq (vmap g1) (vmap g2) /\ guarded_pointwise_relation (Complement _ PE_root) eq (emap g1) (emap g2) /\ g2' = single_vertex_labeledgraph (vmap g2 root) default_DV' default_DE' default_DG'.
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