In constructive type theory it is not a theorem (yet), although by adding a principle of bar induction we can formally prove it. (see http://www.brics.dk/RS/98/39/BRICS-RS-9
My interest in the fan theorem comes from some specific places where it appears, like the completeness theorem of Wim Veldman or giving type-theoretical explanation to backtracking. Hence I am interested in specific instances of it and their computational contents.
I was wondering what is the problem with the general formulation however and that is why I tried to express it in Coq, for the particular fan Cantor space. It boils down to giving a proof of the following:
B : (nat -> option bool) -> Prop
bB : forall a : nat -> bool, exists l : nat, B (IS a l)
mB : forall (a : nat -> bool) (l : nat), B (IS a l) -> B (IS a (S l))
exists n : nat, forall a : nat -> bool, B (IS a n)