Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))

is mentioned by

Thm* eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type. Thm* ydom(f). w=f(y)   P(y,w) Thm*  Thm* ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)

[fpf-all-join-decl]

In prior sections: mb event system 4

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