proposition: Lemma MEP_implies_WF: minimal_element_property -> well_founded R.
proof: Proof. unfold well_founded. unfold minimal_element_property. intro MEP. apply NNPP. intuition. apply not_all_ex_not in H. destruct H. assert (Inhabited [x:T | ~ Acc R x]). exists x. constructor; assumption. apply MEP in H0. destruct H0. destruct H0. destruct H0. contradict H0. constructor. intros. apply NNPP. intuition. apply H1 with y. constructor; assumption. assumption. Qed.
imports: Classical Ensembles EnsemblesImplicit Relation_Definitions Relation_Definitions_Implicit EnsemblesSpec