mb
event
system
5
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
A
:MsgA.
A
||
[ma-empty-compatible-right]
cites the following:
Thm*
eq
:EqDecider(
A
),
B
:Top,
f
:
a
:
A
fp-> Top.
f
||
[fpf-empty-compatible-right]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
5
Sections
EventSystems
Doc
A:MsgA. A || eq:EqDecider(A), B:Top, f:a:A fp-> Top. f || A:MsgA. A || eq:EqDecider(A), B:Top, f:a:A fp-> Top. f ||