proposition: Lemma edge_copy_list_vvalid_mono: forall (G1 G2: Graph) (G1' G2': Graph') g root es P x0, edge_copy_list g root es P (G1, G1') (G2, G2') -> vvalid G1' x0 -> vvalid G2' x0.
proof: Proof. intros. revert G2 G2' H; rev_induction es. + unfold edge_copy_list, relation_list in H; simpl in H. inversion H; subst; auto. + unfold edge_copy_list in H1; rewrite combine_prefixes_app_1, map_app in H1; simpl in H1. apply (proj1 ((proj1 (same_relation_spec _ _) (relation_list_tail _ _)) _ _)) in H1. apply compond_relation_spec in H1. destruct H1 as [[G G'] [? ?]]. eapply (edge_copy_vvalid_mono G G2 G' G2' g); [exact H2 |]. eapply H; eauto. 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