Def P & Q == PQ

is mentioned by

Thm* l:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)	[no_repeats_cons]
Thm* as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||	[zip_length]
Thm* a,b:T, l1,l2:T List. [a / l1]  [b / l2]  a = b & l1  l2	[cons_iseg]
Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)	[member_filter]
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* x1,x2:T, L1,L2:T List. Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2	[cons_sublist_cons]
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))	[member_map]
Thm* l1,l2:T List. (l1 @ l2) = nil  l1 = nil & l2 = nil	[append_is_nil]
Thm* a,a':T, b,b':T List. [a / b] = [a' / b']  a = a' & b = b'	[cons_one_one]
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]
Def L1  L2 Def == f:(||L1||||L2||).  Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)	[sublist]

In prior sections: core int 1 bool 1 int 2 mb nat fun 1 rel 1

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