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

is mentioned by

Thm* es:ES, e,e',ev:E. (ev  [e, e'])  e  ev  & ev  e'	[member-es-interval]
Thm* the_es:ES, e',e:E. (e  before(e'))  (e <loc e')	[member-es-before]
Def a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)	[fpf]

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

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