mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* 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]
cites the following:
0Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A.
Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi
[fpf-join-ap-sq]
4Thm* 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]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 5 Sections EventSystems Doc