Def P  Q == P+Q

is mentioned by

Thm* P:(AAProp), f:(A), L1,L2:A List. Thm* (L1 swap adjacent[P(x,y)] L2) Thm*  Thm* (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) Thm*  filter(f;L1) = filter(f;L2)	[filter_swap_adjacent]
Thm* L:T List, i:(||L||-1), a,b:T. Thm* a before b  swap(L;i;i+1)  a before b  L  a = L[(i+1)] & b = L[i]	[l_before_swap]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x)  (yL.P(y))	[l_exists_cons]

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

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