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  concat(v))
  l:T List. l = u  (l  v) & (x  l)

None

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