proposition: Lemma vcopy1_edge_copy_list_copy: forall (g g1 g2: Graph) g1' g2' root es (M: V -> Prop), vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> (forall v : V, M v \/ ~ M v) -> vcopy1 root g g1 g1' -> edge_copy_list g root es M (g1, g1') (g2, g2') -> copy M root g g2 g2'.
proof: Proof. intros. pose proof triple_vcopy1_edge_copy_list g g1 g2 g1' g2' root es es nil M H H0 H1 H2 (eq_sym (app_nil_r _)) H3 H4 H5. apply triple_final with (es := es); auto. 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