1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. x1 = x2
7. f : ||L1||||L2||
8. increasing(f;||L1||)
9. j:||L1||. L1[j] = L2[(f(j))]
10. j : (||L1||+1)
11. j = 0
  [x1 / L1][j] = [x2 / L2][(f(j-1)+1)]

By:	RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0

1

L1[(j-1)] = L2[(f(j-1)+1-1)]

2 steps

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