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. i1<i
  [x; y]  L

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

1	12. j : 2 13. j = 0   [x; y][j] = L[i1]	1 step
2	12. j : 2 13. j = 0   [x; y][j] = L[i]	1 step

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