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