An exact proof term for the current goal is (λU C x H ⇒ ZF_binunion_closed U C x H {x} (ZF_Sing_closed U C x H)).