Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* eq:EqDecider(A), P:(ATypeProp), x:A, v:Type. Thm* ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)	[fpf-all-single-decl]
Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y	[fpf-single-dom]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom2]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 mb basic rel 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3

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