IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There are as many positive numbers as non-negative.
At:
nat plus ooc nat
~
| By: |
Witness:  x.x-1 | y.y+1 |
Generated subgoal:
| 1 |
InvFuns(;;x.x-1;y.y+1)
 | 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
