is mentioned by

Def M.ef(k,x,s,v,w) Def == E != 1of(2of(2of(2of(2of(M)))))(<k,x>) ==> w = E(s,v)  M.ds(x)

[ma-ef]

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