1. i : 
2. f : {f | i:{z:| z (i,j. i<j) i }  if i=0  else {f(i-1)...} fi}
  if i=0  else {f(i-1)...} fi  Type

By:	AbReduce -1 THEN Assert (j:{k:| k<i }. f(j)  )

1	2. f : {f | i:{z:| z<i }  if i=0  else {f(i-1)...} fi}   j:{k:| k<i }. f(j)	9 steps
2	2. f : {f | i:{z:| z<i }  if i=0  else {f(i-1)...} fi} 3. j:{k:| k<i }. f(j)     if i=0  else {f(i-1)...} fi  Type	3 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html