T:Type, L:T List, n:, f:(n||L||).
  increasing(f;n)  (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))

1	1. T : Type 2. T List 3. n :  4. f : n||nil|| 5. increasing(f;n)   L1:T List.    ||L1|| = n   & increasing(f;||L1||) & (j:||L1||. L1[j] = nil[(f(j))])	7 steps
2	1. T : Type 2. T List 3. u : T 4. v : T List 5. n:, f:(n||v||). 5. increasing(f;n) 5.  5. (L1:T List.  5. (||L1|| = n   & increasing(f;||L1||) & (j:||L1||. L1[j] = v[(f(j))])) 6. n :  7. f : n||[u / v]|| 8. increasing(f;n)   L1:T List.    ||L1|| = n   & increasing(f;||L1||) & (j:||L1||. L1[j] = [u / v][(f(j))])	29 steps

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