IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
lt int eq false elim sqequal
1
1. i :
2. j :
((i<
j) ~ false
) 
i<j
Generated subgoals:
1 |
3. (i< j) ~ false
i<j
 | 2 steps |
2 |
((i< j) ~ false ) Type
 | 3 steps |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html