Def (x  l) == i:. i<||l|| & x = l[i]  T

is mentioned by

Thm* l:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)	[no_repeats_cons]
Thm* P:(T), as:T List, d:T. Thm* ((first a  as s.t. P(a) else d)  as) Thm*  (first a  as s.t. P(a) else d) = d	[find_property]
Thm* l1,l2:T List, x:T. l1  l2  (x  l1)  (x  l2)	[iseg_member]
Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)	[member_filter]
Thm* l:T List, a,x,y:T. Thm* x before y  [a / l]  x = a & (y  l)  x before y  l	[cons_before]
Thm* L:T List, a,b:T. a before b  L  (a  L)	[l_before_member2]
Thm* L:T List, a,b:T. a before b  L  (b  L)	[l_before_member]
Thm* x,y:T, L:T List. Thm* (x  L)  (y  L)  x = y  x before y  L  y before x  L	[l_tricotomy]
Thm* x:T, L:T List. (x  L)  [x]  L	[member_iff_sublist]
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))	[member_map]
Thm* a,x:T. (x  [a])  x = a	[member_singleton]
Thm* L:T List, i:||L||. (L[i]  L)	[select_member]
Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2)	[member_append]
Thm* x:T, l:T List. (y:T. Dec(x = y))  Dec((x  l))	[l_member_decidable]
Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l)	[cons_member]
Thm* L:T List, x:T. (x  L)  null(L)	[member_null]
Thm* L:T List, x:T. null(L)  (x  L)	[null_member]
Thm* x:T. (x  nil)  False	[nil_member]
Thm* as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)	[member_tl]
Thm* a:T List, f:(TT). (x:T. (x  a)  f(x) = x)  map(f;a) = a	[trivial_map]
Thm* a:T List, f,g:(TT'). Thm* (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)	[map_equal2]
Thm* L:T List. L = nil  (x:T. (x  L))	[member_exists]

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