Thanks Raquel! I forgot to update this discussion with its natural answer.

@user21820: "It is unlikely that Terry's note is an unpacking ..." yeah, that was my bet as well

@user21820: thank you, I'll think about this. Still, I think it is interesting to have a more direct path like the one in Terence Tao's note (whether this can be regarded as an unpacking of Shoenfield's theorem in this particular circumstance, I have no idea)

@user21820: I don't really know, it is not my field of expertise. I've just seen the use of Hahn-Banach on a non separable space in the argument above and wondered whether more than DC was truly needed to carry it out. It might be that one could answer `no' by some general principle of which I known nothing about (but I'd like to know more: can you explain or point me to some relevant literature?)

Very interesting, thank you very much

a curiosity: is it really necessary for this argument to work to have at disposal the (weak version of - but still stronger than Countable Dependent) Axiom of Choice? I ask because I don't think anything more than DC is needed to prove both Furstenberg's theorem and Szemerédi's one (but I might be wrong here), thus I find curious that some `serious choice' is needed to bridge them