proposition: Lemma functional_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. apply constructive_indefinite_descr_fun_choice. exact constructive_indefinite_description. Qed.
imports: ChoiceFacts