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

is mentioned by

Thm* l:T List, x:T. (x  l)  (l1,l2:T List. l = (l1 @ [x] @ l2))	[l_member_decomp]
Thm* ll:(T List) List, x:T. (x  concat(ll))  (l:T List. (l  ll) & (x  l))	[member-concat]
Thm* n,i:. i<n  (i  upto(n))	[member_upto2]
Thm* n,i:. (i  upto(n))  i<n	[member_upto]
Thm* P:(TProp).  Thm* (x:T. Dec(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))	[finite-decidable-set]
Thm* P:(TProp).  Thm* (x:T. SqStable(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))	[finite-set-type]
Thm* finite-type(T)  (L:T List. x:T. (x  L))	[finite-type-iff-list]
Thm* L:T List. L  {x:T| (x  L) } List	[list-set-type]
Thm* L:A List, x:A. (A r B)  (x  L)  (x  L)	[l_member_subtype]
Thm* strong-subtype(A;B)  (L:A List, x:B. (x  L)  (x  L))	[strong-subtype-l_member]
Thm* strong-subtype(A;B)  (L:A List, x:B. (x  L)  x  A)	[strong-subtype-l_member-type]

In prior sections: mb list 1 mb list 2

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