T:Type, L1,L2,L3:T List. L1  L2  L2  L3  L1  L3

1	1. T : Type 2. L1 : T List 3. L2 : T List 4. L3 : T List 5. f1 : ||L1||||L2|| 6. increasing(f1;||L1||) 7. j:||L1||. L1[j] = L2[(f1(j))] 8. f : ||L2||||L3|| 9. increasing(f;||L2||) 10. j:||L2||. L2[j] = L3[(f(j))]   increasing(f o f1;||L1||)	1 step
2	1. T : Type 2. L1 : T List 3. L2 : T List 4. L3 : T List 5. f1 : ||L1||||L2|| 6. increasing(f1;||L1||) 7. j:||L1||. L1[j] = L2[(f1(j))] 8. f : ||L2||||L3|| 9. increasing(f;||L2||) 10. j:||L2||. L2[j] = L3[(f(j))] 11. j : ||L1||   L1[j] = L3[(f(f1(j)))]	2 steps

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