proposition: Lemma M0_DEC: forall v, M0 v \/ ~ M0 v.
proof: Proof. intros. destruct (M_DEC v). + left. subst M0. rewrite Union_spec; left; auto. + destruct_eq_dec root v. - left. subst M0. rewrite Union_spec; right; auto. - right. subst M0. rewrite Union_spec. 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