proposition: Lemma MEP_inh_impl_LEM : minimal_element_property -> (exists x y, R y x) -> (forall P : Prop, P \/ ~ P).
proof: Proof. intros ? ? Q. destruct H0 as [x [y Hxy]]. pose (P := Union (Singleton x) (fun a => R y x /\ Q)). specialize (H P). destruct H as [x0]. { exists x. left. constructor. } destruct H. destruct H. 2: { left. apply H. } inversion H; subst; clear H. right. intros ?. unshelve eapply (H0 _ _ Hxy). right. split; assumption. Qed.
imports: Coq(Classical) ZornsLemma(EnsemblesImplicit) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(EnsemblesSpec)