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. apply description_rel_choice_imp_funct_choice. - exact (unique_choice A B). - exact (relational_choice A B). Qed.
imports: ClassicalUniqueChoice RelationalChoice ChoiceFacts