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