IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fincr formation1221 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
By:
Witness 1
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:
