An exact proof term for the current goal is (λU C X HX Y HY ⇒ ZF_Union_closed U C {X,Y} (ZF_UPair_closed U C X HX Y HY)).