IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq int is eq nsub
1
1. b : 
IsEqFun(b;
i,j. i=j)
| By: |
Def THEN SOReduce Concl |
Generated subgoal:
| 1 |
 x,y:b. x=y   x = y
 | 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
