proposition: Lemma copy_invalid_refl: forall (g: Graph) M root (src0 dst0: E' -> V'), ~ vvalid g root -> copy M root g g (empty_labeledgraph src0 dst0 default_DV' default_DE' default_DG').
proof: Proof. intros. unfold copy. assert (Same_set (reachable_by g root (Complement V M)) (Empty_set _)). 1: { rewrite Same_set_spec; intros ?. rewrite Empty_set_spec. pose proof reachable_by_head_valid g root a (Complement V M); tauto. } rewrite H0. rewrite weak_edge_prop_Empty, Intersection_Empty_left. rewrite !image_Empty. split; [| split; [| split; [| split; [| split; [| split]]]]]. + reflexivity. + reflexivity. + reflexivity. + simpl. rewrite Same_set_spec; intros ?. rewrite Empty_set_spec; tauto. + simpl. rewrite Same_set_spec; intros ?. rewrite Empty_set_spec; tauto. + simpl. intros ? ? ? ?. inversion H1. + simpl. apply guarded_bij_empty_empty. 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