1. T : Type
2. x : T
3. y : T
4. L : T List
5. i1 : 
6. i1<||L||
7. x = L[i1]
8. i : 
9. i<||L||
10. y = L[i]
11. i<i1
  [y; x]  L

By:	Unfold `sublist` 0 THEN Reduce 0 THEN InstConcl [j.if j=0 i else i1 fi] THEN Reduce 0 THEN Try (Unfold `label` 0 THEN Reduce 0)

1	increasing(j.if j=0 i else i1 fi;2)	1 step
2	12. j : 2   [y; x][j] = L[if j=0 i else i1 fi]	3 steps

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