LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm*  (x:Ay:BQ(x,y))  (f:(AB). x:AQ(x,f(x)))[ax_choice_version3]
cites the following:
1Thm*  (x:Ay:BQ(x,y))  (f:(AB). x:AQ(x,f(x)))[ax_choice_version2]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
LogicSupplement Sections DiscrMathExt Doc