1. n : 
2. x : n
3. y : n
4. x<y
  f:(2||upto(n)||). increasing(f;2) & (j:2. [x; y][j] = upto(n)[(f(j))])

By:	RWO Thm* n:. ||upto(n)|| ~ n 0 THEN InstConcl [i.if i=0 x else y fi]

1	increasing(i.if i=0 x else y fi;2)   & (j:2. [x; y][j] = upto(n)[((i.if i=0 x else y fi)(j))])	6 steps
2	5. f : 2n 6. j : 2   f(j)<||upto(n)||	1 step

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