forall (X Y : HSet) (R : X -> Y -> HProp), (forall x, hexists (R x)) -> hexists (fun f => forall x, R x (f x)).
From HoTT Require Import ExcludedMiddle canonical_names. From HoTT Require Import HIT.unique_choice. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals.