1. T : Type
2. T List
3. u : T
4. v : T List
5. bs:T List. rev(v @ bs) = (rev(bs) @ rev(v))
6. bs : T List
  ((rev(bs) @ rev(v)) @ [u]) = (rev(bs) @ rev(v) @ [u])

By:	RWO Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs)) 0

None

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