proposition: Lemma guarded_morphism_disjointed_union: forall PV1 PE1 PV2 PE2 vmap emap (G: PreGraph V E) (G': PreGraph V' E'), guarded_morphism PV1 PE1 vmap emap G G' -> guarded_morphism PV2 PE2 vmap emap G G' -> boundary_consistent PV1 PV2 PE1 PE2 vmap emap G G' -> guarded_morphism (Union _ PV1 PV2) (Union _ PE1 PE2) vmap emap G G'.
proof: Proof. intros. destruct H1 as [[? ?] [? ?]]. split; intros. + rewrite Union_spec in *. destruct H5; [apply (vvalid_preserved H) | apply (vvalid_preserved H0)]; auto. + rewrite Union_spec in *. destruct H5; [apply (evalid_preserved H) | apply (evalid_preserved H0)]; auto. + rewrite Union_spec in H5, H6. destruct H5, H6; [ apply (src_preserved H) | apply H1 | apply H3 | apply (src_preserved H0)]; auto. + rewrite Union_spec in H5, H6. destruct H5, H6; [ apply (dst_preserved H) | apply H2 | apply H4 | apply (dst_preserved H0)]; 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.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation