Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* no_repeats(T;nil)	[no_repeats_nil]
Thm* l:T List, x,y,z:T. Thm* no_repeats(T;l)  x before y  l  y before z  l  x before z  l	[l_before_transitivity]
Thm* L1,L2,L:T List, x:T. Thm* no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L	[append_overlapping_sublists]
Thm* l:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)	[no_repeats_cons]
Thm* l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)	[no_repeats_iff]
Thm* P:(T), as:T List, d:T. Thm* ((first a  as s.t. P(a) else d)  as) Thm*  (first a  as s.t. P(a) else d) = d	[find_property]
Thm* as:(T1T2) List. zip(1of(unzip(as));2of(unzip(as))) = as	[zip_unzip]
Thm* as:T1 List, bs:T2 List. ||as|| = ||bs||    unzip(zip(as;bs)) = <as,bs>	[unzip_zip]
Thm* as:T1 List, bs:T2 List. ||as|| = ||bs||    ||zip(as;bs)|| = ||as||	[length_zip]
Thm* as:T1 List, bs:T2 List, i:. Thm* i<||zip(as;bs)||  zip(as;bs)[i] = <as[i],bs[i]>	[select_zip]
Thm* as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||	[zip_length]
Thm* T1,T2:Type, as:T1 List, bs:T2 List. zip(as;bs)  (T1T2) List	[zip_wf]
Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l)  T'	[list_accum_wf]
Thm* L_1,L_2:T List. L_1  L_2  L_1  L_2	[iseg_is_sublist]
Thm* l1,l2:T List. l1  l2  ||l1||||l2||	[iseg_length]
Thm* P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)	[filter_iseg]
Thm* L:T List. L  nil  null(L)	[iseg_nil]
Thm* l1,l2:T List, x:T. l1  l2  (x  l1)  (x  l2)	[iseg_member]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Thm* l:T List. nil  l	[nil_iseg]
Thm* l:T List. l  l	[iseg_weakening]
Thm* l1,l2,l3:T List. l2  l3  l1  l2  l1  l3	[iseg_transitivity2]
Thm* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))	[firstn_is_iseg]
Thm* l1,l2,l3:T List. l1  l2  l1  l2 @ l3	[iseg_append]
Thm* l1,l2,l3:T List. l1  l2  l2  l3  l1  l3	[iseg_transitivity]
Thm* a,b:T, l1,l2:T List. [a / l1]  [b / l2]  a = b & l1  l2	[cons_iseg]
Thm* f:(T1T2), Q:(T2), L:T1 List. Thm* filter(Q;map(f;L)) = map(f;filter(Q o f;L))	[filter_map]
Thm* P:(T), l:T List. filter(P;l)  {x:T| P(x) } List	[filter_type]
Thm* P1,P2:(T), L:T List. Thm* filter(P1;filter(P2;L)) ~ filter(t.(P1(t))(P2(t));L)	[filter_filter]
Thm* P:(T), l1,l2:T List. filter(P;l1 @ l2) ~ (filter(P;l1) @ filter(P;l2))	[filter_append]
Thm* L:A List, f1,f2:(A). f1 = f2  (filter(f1;L) ~ filter(f2;L))	[filter_functionality]
Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)	[member_filter]
Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List	[map_wf_listp]
Thm* l:A List. ||l||1	[listp_properties]
Thm* l:T List, a,x,y:T. Thm* x before y  [a / l]  x = a & (y  l)  x before y  l	[cons_before]
Thm* L:T List, a,b:T. a before b  L  (a  L)	[l_before_member2]
Thm* x,y:T. x before y  nil  False	[nil_before]
Thm* L:T List, a,b:T. a before b  L  (b  L)	[l_before_member]
Thm* x,y:T, L:T List. Thm* (x  L)  (y  L)  x = y  x before y  L  y before x  L	[l_tricotomy]
Thm* x:T, L:T List. (x  L)  [x]  L	[member_iff_sublist]
Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L	[sublist_pair]
Thm* L1,L2:T List. null(L2)  L1  tl(L2)  L1  L2	[sublist_tl]
Thm* L:T List. L  nil  L = nil	[sublist_nil]
Thm* L1,L2:T List. L1 = L2  L1  L2	[sublist_weakening]
Thm* x1,x2:T, L1,L2:T List. Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2	[cons_sublist_cons]
Thm* L:T List. nil  L  True	[nil_sublist]
Thm* L1,L2:T List. L1  L2  L2  L1  L1 = L2	[sublist_antisymmetry]
Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2	[proper_sublist_length]
Thm* x:T, L:T List. [x / L]  nil  False	[cons_sublist_nil]
Thm* L1,L2:T List. L1  L2  ||L1||||L2||	[length_sublist]
Thm* L1,L2,L3:T List. L1  L2  L2  L3  L1  L3	[sublist_transitivity]
Thm* L:T List, x:T. null(L)  last([x / L]) = last(L)	[last_cons]
Thm* T:Type, L:T List. null(L)  last(L)  T	[last_wf]
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))	[member_map]
Thm* a,x:T. (x  [a])  x = a	[member_singleton]
Thm* L:T List, i:||L||. (L[i]  L)	[select_member]
Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2)	[member_append]
Thm* x:T, l:T List. (y:T. Dec(x = y))  Dec((x  l))	[l_member_decidable]
Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l)	[cons_member]
Thm* L:T List, x:T. (x  L)  null(L)	[member_null]
Thm* L:T List, x:T. null(L)  (x  L)	[null_member]
Thm* x:T. (x  nil)  False	[nil_member]
Thm* as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)	[member_tl]
Thm* a:T List, f:(TT). (x:T. (x  a)  f(x) = x)  map(f;a) = a	[trivial_map]
Thm* a:T List, f,g:(TT'). Thm* (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)	[map_equal2]
Thm* L:T List. L = nil  (x:T. (x  L))	[member_exists]
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* l:T List. (l @ nil) ~ l	[append_nil_sq]
Thm* l1,l2:T List. (l1 @ l2) = nil  l1 = nil & l2 = nil	[append_is_nil]
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,a':T, b,b':T List. [a / b] = [a' / b']  a = a' & b = b'	[cons_one_one]
Thm* Q:((T List)Prop).  Thm* Q(nil)  (ys:T List, x:T. Q(ys)  Q(ys @ [x]))  (zs:T List. Q(zs))	[list_append_singleton_ind]
Thm* L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x]))	[list_decomp_reverse]
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* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))	[map_append_sq]
Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])	[nth_tl_decomp]
Thm* L:T List. 0<||L||  (L ~ [hd(L) / tl(L)])	[list_decomp]
Thm* l:T List. ||l|| = 0    l = nil	[length_zero]
Thm* L:T List. L = nil  0<||L||	[non_nil_length]
Thm* L:T List, P:(||L||Prop). Thm* (x:||L||. Dec(P(x))) Thm*  Thm* (i,j:||L||. P(i)  i<j  P(j)) Thm*  Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))	[append_split2]
Thm* L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L	[append_firstn_lastn]
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]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 mb basic rel 1 mb nat

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