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