proposition: Lemma disjointed_guard_left_union: forall {V E} (PV1 PV2 PV3: V -> Prop) (PE1 PE2 PE3: E -> Prop), disjointed_guard (Union _ PV1 PV2) PV3 (Union _ PE1 PE2) PE3 -> disjointed_guard PV1 PV3 PE1 PE3 /\ disjointed_guard PV2 PV3 PE2 PE3.
proof: Proof. intros. destruct H. rewrite Union_left_Disjoint in H, H0. split; split; 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