proposition: Lemma PV1_DEC: forall v, PV1 v \/ ~ PV1 v.
proof: Proof. clear PE1 H_PE1. intros. subst M_rec. destruct (Mr_DEC v) as [[|]|]. + right. intro. subst PV1. apply reachable_by_through_set_foot_prop in H0. apply H0, H. + left; apply H. + right. intro; apply H. rewrite Union_spec; right; apply H0. 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