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][0]

By:	HypSubstSq -1 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