mb event system 4 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def eqof(d) == 1of(d)

is mentioned by

Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v) ~ (eqof(eq)(y,x))[fpf-single-dom-sq]
Thm* eq:EqDecider(A), x,y:A, v,z:Top.
Thm* x : v(y)?z ~ if eqof(eq)(x,y) v else z fi		[fpf-cap-single]

In prior sections: mb event system 2

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

mb event system 4 Sections EventSystems Doc