proposition: Lemma labeledgraph_vgen_vcopy1: forall (G: Graph) x x0, vcopy1 x G (labeledgraph_vgen G x x0) (single_vertex_labeledgraph (vmap (labeledgraph_vgen G x x0) x) default_DV' default_DE' default_DG') /\ co_vertex x0 = vmap (labeledgraph_vgen G x x0) x.
proof: Proof. intros. split. + split; [| split; [| split]]. - reflexivity. - apply guarded_pointwise_relation_spec; intros. simpl. unfold labeledgraph_vgen, update_vlabel, vmap; simpl. destruct_eq_dec x x1; [congruence | auto]. - apply guarded_pointwise_relation_spec; intros. auto. - reflexivity. + simpl. unfold labeledgraph_vgen, update_vlabel, vmap; simpl. destruct_eq_dec x x; [auto | congruence]. 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