Def  == {i:| 0i }

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* n:, f:(nT), i:n. mklist(n;f)[i] = f(i)	[mklist_select]
Thm* n:, f:(nT). ||mklist(n;f)|| = n	[mklist_length]
Thm* z:T List. ||z|| = 2    z = [z[0]; z[1]]	[list_2_decomp]
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||	[map_length_nat]
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 (x  l) == i:. i<||l|| & x = l[i]  T	[l_member]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1 mb nat

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