IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat ind12 1. P : Prop
2. P(0)
3. i:. P(i-1) P(i)
4. j : 5. 0<j 6. P(j-1)
P(j)
By:
BackThru 3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
i:
. P(i-1) 
P(i)
P(j)
