Def A & B == AB

is mentioned by

Thm* R:(TTProp), k:, x,y:T. Thm* (x R^k y) Thm*  Thm* (L:T List.  Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))	[rel_exp_list]
Thm* L:T List, n:, f:(n||L||). Thm* increasing(f;n) Thm*  Thm* (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))	[range_sublist]
Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'. Thm* (x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))	[member_map_filter]

In prior sections: mb basic mb nat mb list 1

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