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

By:	Assert (j:{k:| k<i }. f(j)  )

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

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