1. T : Type
2. ll1 : (T List) List
3. ll2 : (T List) List
4. l : (T List) List
5. ll2 = (ll1 @ l)
  l@0:T List. concat(ll1 @ l) = (concat(ll1) @ l@0)

By:	RWO Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2)) 0 THEN InstConcl [concat(l)]

None

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