The feedback I am getting suggests that the truth of the matter is that
NGB + global choice is an extension of NGB + set choice that is
conservative for the language of pure sets.
Can anyone confirm this, preferably with a reference?
thanks
Thomas