mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def (x  l) == i:. i<||l|| & x = l[i]  T

is mentioned by

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]
Def (xL.P(x)) == x:T. (x  L) & P(x)[l_exists]
Def (xL.P(x)) == x:T. (x  L)  P(x)[l_all]
Def l_disjoint(T;l1;l2) == x:T. ((x  l1) & (x  l2))[l_disjoint]

In prior sections: mb list 1

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

mb list 2 Sections MarkB generic Doc