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

is mentioned by

Thm* x:A. (x,y:A. Dec(x = y))  (L:A List. Dec((x  L)))	[decidable__l_member]
Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L)	[assert-deq-member]

In prior sections: mb list 1 mb list 2 mb event system 1

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