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)) @ map(f;[t]))

By:	Reduce 0 THEN RWO Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2)) 0 THEN Analyze

1	concat(map(f;upto(t))) ~ concat(map(f;upto(t)))	Auto
2	(f(t)) ~ concat([(f(t))])	1 step

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