IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fincr formation122231 1. i : 2. f : {f | i:{i1:| i1 (i,j. i<j) i } if i=0 else {f(i-1)...} fi}
3. j:{k:| k<i }. f(j) 4. i 0
5. f(i-1)
By:
With (i-1) (Analyze -3)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
i,j. i<j) i } 
if i=
0
else {f(i-1)...} fi}
j:{k:
0
f(i-1) 
