[FOM] Sperner's lemma and Bishop style constructive mathematics

[ochibocho2]

I am Yasuhito Tanaka at Doshisha University in Japan.

Simpson's book "Subsystems of Second Order Arithmetic" states that 
Sperner's Lemma is provable in RCA_0.

Then, is Sperner's lemma provable in Bishop style constructive 
mathematics or mathematics with intuitionistic logic?
--------------------------------------
Get the new Internet Explorer 8 optimized for Yahoo! JAPAN
http://pr.mail.yahoo.co.jp/ie8/