T:Type, ll:(T List) List, x:T.
  (x  concat(ll))  (l:T List. (l  ll) & (x  l))

By:	((InductionOnList THEN Unfold `concat` 0 THEN Reduce 0 ((THEN ((Try (Fold `concat` 0)) (THEN ((RWW Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2) 0) (THEN ((RWW Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0)) THEN RWW Thm* x:T. (x  nil)  False 0 THEN ExRepD

1	1. T : Type 2. (T List) List 3. u : T List 4. v : (T List) List 5. x:T. (x  concat(v))  (l:T List. (l  v) & (x  l)) 6. x : T 7. (x  u)  (x  concat(v))   l:T List. l = u  (l  v) & (x  l)	3 steps
2	1. T : Type 2. (T List) List 3. u : T List 4. v : (T List) List 5. x:T. (x  concat(v))  (l:T List. (l  v) & (x  l)) 6. x : T 7. l : T List 8. l = u  (l  v) 9. (x  l)   (x  u)  (x  concat(v))	4 steps

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