An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → {F x|x ∈ X} ∈ U) (λ_ _ H ⇒ H)).