Def p = q == 1of(p) = 1of(q)(2of(p)=2of(q))

is mentioned by

Thm* the_w:World, e,e':E. e = e'  e = e'	[assert-w-eq-E-iff]
Thm* the_w:World, e,e':E. e = e'  e = e'	[assert-w-eq-E]

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