proposition: Lemma vcopy1_edge_copy_list_mapped_root_edge_evalid: forall (g g1 g2: Graph) (g1' g2': Graph') root es es_done es_later (M: V -> Prop), vvalid g root -> ~ M root -> (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ es_later -> (forall v : V, M v \/ ~ M v) -> vcopy1 root g g1 g1' -> edge_copy_list g root es_done M (g1, g1') (g2, g2') -> forall e', In e' (map (emap g2) es_done) -> evalid g2' e'.
proof: Proof. intros. rewrite in_map_iff in H7. destruct H7 as [e [? ?]]. pose proof triple_vcopy1_edge_copy_list g g1 g2 g1' g2' root es es_done _ M H H0 H1 H2 H3 H4 H5 H6. destruct H9 as [? [? _]]. pose proof evalid_preserved H9 e. subst e'. rewrite <- H11. + rewrite <- (proj1 (proj2 H10)). clear - H1 H3 H8. rewrite H3 in H1. specialize (H1 e). rewrite in_app_iff in H1. pose proof (proj1 H1 (or_introl H8)). destruct H; auto. + rewrite Union_spec; right. 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