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
12. j : 2
13. j = 0
  [y; x][j] = L[i1]

By:	RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0 THEN Try (Unfold `label` 0 THEN Reduce 0) THEN RWO Thm* a:T, as:T List, i:. i0  [a / as][i] = a 0

None

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