An exact proof term for the current goal is (λX x : set ⇒ iffEL (x ∈ ⋃ X) (∃Y : set, x ∈ Y ∧ Y ∈ X) (UnionEq X x)).