proposition: Lemma triple_vcopy1: forall (g1 g2: Graph) (g2': Graph') root, vvalid g1 root -> vcopy1 root g1 g2 g2' -> guarded_bij (eq root) (Empty_set _) (vmap g2) (emap g2) g2 g2'.
proof: Proof. intros g1 g2 g2' root ? [VCOPY_si [VCOPY_gprv [VCOPY_gpre ?]]]. subst g2'. split; [.. | split]; intros. + apply is_guarded_inj_single. + apply is_guarded_inj_empty. + subst v. unfold single_vertex_labeledgraph, single_vertex_pregraph; simpl. destruct_eq_dec (vmap g2 root) (vmap g2 root); [| congruence]. rewrite (proj1 VCOPY_si) in H. tauto. + inversion H0. + inversion H0. + inversion H0. 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