1. T : Type
2. (T List) List
  n:||concat(nil)||. 
  m:||nil||. 
  ||concat(firstn(m;nil))||n
  & n-||concat(firstn(m;nil))||<||nil[m]||
  & concat(nil)[n] = nil[m][(n-||concat(firstn(m;nil))||)]  T

None

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