1. T : Type
2. x : T
3. L : T List
4. i : 
5. i<||L||
6. x = L[i]
  f:(1||L||). increasing(f;1) & (j:1. [x][j] = L[(f(j))])

By:	InstConcl [x.i] THEN Try (Unfold `label` 0 THEN Reduce 0)

1	increasing(x.i;1)	1 step
2	7. j : 1   [x][j] = L[((x.i)(j))]	1 step

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