proposition: Lemma labeledgraph_egen_ecopy1_not_vvalid: forall (g1: Graph) (g1': Graph') e e' src' dst', ~ evalid g1' (co_edge e') -> src' = vmap g1 (src g1 e) -> ~ vvalid g1' dst' -> ~ vvalid g1 (dst g1 e) -> ecopy1 e (g1, g1') (labeledgraph_egen g1 e e', labeledgraph_add_edge g1' (co_edge e') src' dst' default_DE').
proof: Proof. intros ? ? ? ? ? ? HH0 HH1 HH2 HH3. subst src'. split; [| split; [| split; [| split; [| split]]]]. + reflexivity. + intros v; reflexivity. + rewrite guarded_pointwise_relation_spec; intros. unfold emap, labeledgraph_egen, update_elabel; simpl. destruct_eq_dec e x; auto. unfold Complement, Ensembles.In in H; congruence. + split; [| split; [| split]]; simpl. - apply Prop_join_Empty. - unfold emap, labeledgraph_egen, update_elabel, addValidFunc; simpl. destruct_eq_dec e e; [| congruence]. apply Prop_join_x1; auto. - unfold emap, labeledgraph_egen, updateEdgeFunc, addValidFunc; simpl. intros. destruct_eq_dec (co_edge e') e0; auto. subst; exfalso; auto. - unfold emap, labeledgraph_egen, updateEdgeFunc, addValidFunc; simpl. intros. destruct_eq_dec (co_edge e') e0; auto. subst; exfalso; auto. + simpl. unfold vmap, emap, labeledgraph_egen, updateEdgeFunc, update_elabel; simpl. destruct_eq_dec e e; [| congruence]. destruct_eq_dec (co_edge e') (co_edge e'); [| congruence]. auto. + simpl; intros. exfalso; 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