proposition: Lemma aux00: Same_set (Union _ PV1 (Complement _ PV1)) (Full_set _).
proof: Proof. rewrite Same_set_spec; intro v. rewrite Union_spec; unfold Complement, Ensembles.In. pose proof PV1_DEC. clear -H. firstorder; constructor. 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