mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* x,y:Id, k:Knd, A,B,T:Type, f:(ABTA).
Thm* y = x  ma-single-effect1(x;A;y;B;k;T;f MsgA
[ma-single-effect1_wf]
cites the following:
4Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:Az:Top.
Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi
[fpf-join-cap-sq]
0Thm* eq:EqDecider(A), x,y:Av:Top. x  dom(y : v x = y[fpf-single-dom]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 5 Sections EventSystems Doc