proposition: Lemma ecopy1_evalid_mono: forall (G1 G2: Graph) (G1' G2': Graph') e e0, ecopy1 e (G1, G1') (G2, G2') -> evalid G1' e0 -> evalid G2' e0.
proof: Proof. intros. destruct H as [_ [_ [_ [? _]]]]. eapply pregraph_join_vealid_mono; 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