An exact proof term for the current goal is (SepE2 (𝒫 (∑x ∈ X, ⋃ (Y x))) (λf ⇒ ∀x ∈ X, f x ∈ Y x) f Hf x).