1. T : Type
2. L1 : T List
3. L2 : T List
4. L1  L2
5. ||L1|| = ||L2||
6. i : 
7. i<||L1||
  L1[i] = L2[i]

1

4. f : ||L1||||L2|| 5. increasing(f;||L1||) 6. j:||L1||. L1[j] = L2[(f(j))] 7. ||L1|| = ||L2||   8. i :  9. i<||L1|| 10. L1[i] = L2[(f(i))]   L1[i] = L2[i]

2 steps

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