Def e@i.P(e) == e:E. loc(e) = i  Id  P(e)

is mentioned by

Thm* es:ES, i,x:Id, T:Type, I:(TProp). Thm* (vartype(i;x) r T) & e@i.first(e)  I((x when e)) Thm*  Thm* e@i.I((x when e))  I((x after e))  @i always.I(x)	[es-invariant1]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). Thm* e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e)	[alle-at-iff]
Def @i always.P(v) == e@i.P((x when e))	[alle-at1]

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