IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat not finite
2
1. 
n:
. ( ~ n) 
( ~ (n+1))
Finite()
| By: |
Analyze THEN Analyze-1 |
Generated subgoal:
| 1 |
2. n :
3. ~ n
False
 | 3 steps |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
