Def P & Q == PQ

is mentioned by

Thm* ll:(T List) List, x:T. (x  concat(ll))  (l:T List. (l  ll) & (x  l))	[member-concat]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* f:(TT'), L:T List, x',y':T'. Thm* x' before y'  map(f;L)  (x,y:T. x before y  L & f(x) = x' & f(y) = y')	[before-map]
Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))	[mu-property]
Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y))	[pairwise-cons]

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

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