proposition: Theorem choice : forall (A B : Type) (R : A->B->Prop), (forall x : A, exists y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)).
proof: Proof. intros A B R H. exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))). intro x. apply (proj2_sig (constructive_indefinite_description _ (H x))). Qed.
imports: Classical ChoiceFacts