Def A & B == AB

is mentioned by

Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Def (x  l) == i:. i<||l|| & x = l[i]  T	[l_member]

In prior sections: mb basic mb nat

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