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

By:	RWO Thm* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll)) 0 THEN Reduce 0 THEN RWO Thm* l:T List. (l @ nil) ~ l 0

None

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