is mentioned by

Thm* as:T1 List, bs:T2 List, i:. Thm* i<||zip(as;bs)||  zip(as;bs)[i] = <as[i],bs[i]>	[select_zip]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L	[sublist_pair]
Thm* L:T List, i:||L||. (L[i]  L)	[select_member]
Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i)	[mklist_select]
Thm* z:T List. ||z|| = 2    z = [z[0]; z[1]]	[list_2_decomp]
Thm* a:T List, f,g:(TT'). Thm* (i:. i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a)	[map_equal]
Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b	[list_extensionality]
Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])	[nth_tl_decomp]
Def no_repeats(T;l) == i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]  T	[no_repeats]
Def L1  L2 Def == f:(||L1||||L2||).  Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)	[sublist]
Def last(L) == L[(||L||-1)]	[last]
Def (x  l) == i:. i<||l|| & x = l[i]  T	[l_member]

In prior sections: list 1 mb basic mb nat

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