proposition: Lemma aux08: Disjoint _ (eq root) PV0.
proof: Proof. intros. rewrite H_PV0. rewrite Disjoint_spec. intros. subst x M_rec. rewrite <- Intersection_Complement in H0. apply reachable_by_foot_prop in H0. rewrite H_M0 in H0. rewrite !Intersection_spec in H0. apply (proj1 H0); right; 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