1. T : Type
2. f : (T List)
3. t : 
4. t' : 
5. t<t'
6. t+1 = 0
  (concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t+1-1) @ [(t+1-1)]))

1

(concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t) @ [t]))

4 steps

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