proposition: Lemma aux06: Disjoint _ PV1 PV0.
proof: Proof. intros. rewrite H_PV0, H_Mrec, H_PV1. rewrite Disjoint_spec; intros. rewrite <- Intersection_Complement in H0. apply reachable_by_foot_prop in H0. rewrite Intersection_spec in H0; unfold Complement, Ensembles.In in H0. 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