mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def e = e' == eqof(1of(2of(es)))(e,e')

is mentioned by

Thm* the_es:ES, e,e':E. e = e'  e = e'[assert-es-eq-E]

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

mb event system 2 Sections EventSystems Doc