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
9. (x  l)
  (x  u)  (x  concat(v))

None

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