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;![](FONT/lam.png)
i,j. i=
j)
By: |
Def THEN SOReduce Concl |
Generated subgoal:
1 |
x,y: b. x= y ![](FONT/if_big.png) x = y
![](FONT/BLANK.png) | 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html