proposition: Lemma aux02: Same_set PE3 (Union _ PE1 PE0).
proof: Proof. intros. rewrite H_PE0, H_PE3, H_PE1. rewrite aux01 by auto. rewrite weak_edge_prop_Union. rewrite Intersection_Union_distr_l. reflexivity. 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