IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc ycomb typing demo
1
2
1
1
1. T : Type
2. F :
k:
. (
k
T)

(k+1)
T
Y(F)
0
T
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html