IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc ycomb typing demo1221 1. T : Type
2. F : k:. (kT)(k+1)T 3. n:. Y(F) nT 4. x : Y(F,x) T
By:
Witness3: x+1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
k:
. (
T)
n:
Y(F,x) 
