IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat descent
1
1. P : 
Prop
2. 
x:. P(x) 
(
x':. x'<x & P(x'))
(x:. P(x))
| By: |
Analyze THEN Analyze3 |
Generated subgoal:
| 1 |
3. x :
4. P(x)
False
 | 4 steps |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
