proposition: Lemma aux03: Same_set PE3_root (Union _ PE1_root (eq e0)).
proof: Proof. intros. rewrite H_PE3r, H_PE1r. rewrite Same_set_spec; intro e. rewrite Union_spec, in_app_iff; simpl. 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.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism