Def e  e'  == (e <loc e')  e = e'  E

is mentioned by

Thm* es:ES, e,e':E. e  e'   loc(e) = loc(e')  Id	[es-le-loc]
Thm* the_es:ES. Trans x,y:E. x  y	[es-le-trans]

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