proposition: Lemma guarded_bij_disjointed_weak_edge_prop_union: forall PV1 PV2 vmap emap (G: PreGraph V E) (G': PreGraph V' E'), let PE1 := Intersection _ (weak_edge_prop PV1 G) (evalid G) in let PE2 := Intersection _ (weak_edge_prop PV2 G) (evalid G) in disjointed_guard (image_set PV1 vmap) (image_set PV2 vmap) (image_set PE1 emap) (image_set PE2 emap) -> guarded_bij PV1 PE1 vmap emap G G' -> guarded_bij PV2 PE2 vmap emap G G' -> boundary_dst_consistent PE1 PV2 vmap emap G G' -> boundary_dst_consistent PE2 PV1 vmap emap G G' -> guarded_bij (Union _ PV1 PV2) (Union _ PE1 PE2) vmap emap G G'.
proof: Proof. intros. apply guarded_bij_disjointed_union; auto. destruct H. assert (Disjoint _ PV1 PV2) by (eapply image_Disjoint_rev; eauto). split; split; auto; hnf; intros. + rewrite Disjoint_spec in H5. unfold PE1, weak_edge_prop in H6; rewrite Intersection_spec in H6. pose proof H5 _ (proj1 H6) H7; tauto. + rewrite Disjoint_spec in H5. unfold PE2, weak_edge_prop in H6; rewrite Intersection_spec in H6. pose proof H5 _ H7 (proj1 H6); tauto. 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.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation