An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λg : set ⇒ function_on g X Y) f Hf).