proposition: Lemma MEP_implies_WF: minimal_element_property -> well_founded R.
proof: Proof. intros MEP. red. intros. constructor. intros. unshelve epose proof (MEP_inh_impl_LEM MEP _) as LEM. { eauto. } destruct (LEM (Acc R y)) as [|]; try assumption. exfalso. assert (Inhabited [x:T | ~ Acc R x]) as HInh. { exists y. constructor; assumption. } apply MEP in HInh as [? [[?] ?]]. contradict H1. constructor. intros. destruct (LEM (Acc R y0)) as [|]; try assumption. exfalso. apply H2 with y0. - constructor; assumption. - assumption. Qed.
imports: Coq(Classical) ZornsLemma(EnsemblesImplicit) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(EnsemblesSpec)