T:Type, L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L

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

1	1. T : Type 2. L : T List 3. i : ||L|| 4. j : ||L|| 5. i<j 6. i@0 : 1   if i@0=0 i else j fi<if i@0+1=0 i else j fi	1 step
2	1. T : Type 2. L : T List 3. i : ||L|| 4. j : ||L|| 5. i<j 6. j@0 : 2   [L[i]; L[j]][j@0] = L[if j@0=0 i else j fi]	2 steps

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