fact: Definition ecopy1 e (p1 p2: Graph * Graph') := let (g1, g1') := p1 in let (g2, g2') := p2 in g1 ~=~ g2 /\ pointwise_relation V eq (vmap g1) (vmap g2) /\ guarded_pointwise_relation (Complement _ (eq e)) eq (emap g1) (emap g2) /\ pregraph_join (Empty_set _) (eq (emap g2 e)) g1' g2' /\ (vvalid g1 (src g2 e) -> vmap g2 (src g2 e) = src g2' (emap g2 e)) /\ (vvalid g1 (dst g2 e) -> vmap g2 (dst g2 e) = dst g2' (emap g2 e)).
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