proposition: Lemma aux01: Same_set PV3 (Union _ PV1 PV0).
proof: Proof. clear PE1 PE3 PE0 H_PE1 H_PE3 H_PE0. intros. rewrite H_PV0, H_Mrec, H_PV3. rewrite map_app; simpl map. rewrite reachable_by_through_app_strong' by (rewrite <- H_PV1; apply aux00). rewrite reachable_by_through_singleton'. subst PV1. rewrite Intersection_Complement. 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