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) @ [t]))

By:	RWO Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as')) 0

1

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

3 steps

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