is mentioned by

Thm* ll:(T List) List, n:||concat(ll)||. Thm* m:||ll||.  Thm* ||concat(firstn(m;ll))||n Thm* & n-||concat(firstn(m;ll))||<||ll[m]|| Thm* & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]	[select_concat]
Thm* P:(TProp), A,B:T List. Thm* A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List	[list-eq-set-type]
Thm* m:, n:m. upto(m)[n] = n	[select_upto]
Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))	[select-map]
Thm* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]	[last_l_interval]
Thm* l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]	[hd_l_interval]
Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]	[select_l_interval]
Def (x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])	[pairwise]
Def l_interval(l;j;i) == mklist(i-j;x.l[(j+x)])	[l_interval]

In prior sections: list 1 mb basic mb nat mb list 1 mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html