IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
complete nat ind
1
1. P : 
Prop
2. 
i:. (j:i. P(j)) 
P(i)
3. i :
P(i)
Generated subgoal:
| 1 |
4. i1:i. P(i1)
P(i)
 | 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
