1. T : Type
2. (T List) List
3. 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  v)
9. (x  l)
  l:T List. (l  v) & (x  l)

None

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