proposition: Lemma WO_implies_AC: forall (A B:Type) (R: A -> B -> Prop) (WO:relation B), well_order WO -> (forall x:A, exists y:B, R x y) -> exists f:A->B, forall x:A, R x (f x).
proof: Proof. intros. assert (forall a:A, Inhabited [ b:B | R a b ]). intro. pose proof (H0 a). destruct H1. exists x. constructor; assumption. exists (fun a:A => proj1_sig (WO_minimum WO H [ b:B | R a b ] (H1 a))). intro. destruct @WO_minimum. simpl. destruct a. destruct H2. assumption. Qed.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec