An exact proof term for the current goal is (λU C ⇒ ZF_closed_E U C (∀X ∈ U, ⋃ X ∈ U) (λH _ _ ⇒ H)).