 where FT\(_?\) is some form of Brouwer’s fan theorem, and \(T\) is a theorem of INT. To do so, we need to distinguish between certain types of bar for the complete binary fan \(2^*\) (the set of all finite sequences in \(\{0,1\})\). 