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-left]
cites the following:
Thm*
eq
:EqDecider(
A
),
B
:Top,
f
:
a
:
A
fp-> Top. ||
f
[fpf-empty-compatible-left]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
5
Sections
EventSystems
Doc
A:MsgA. || Aeq:EqDecider(A), B:Top, f:a:A fp-> Top. || fA:MsgA. || Aeq:EqDecider(A), B:Top, f:a:A fp-> Top. || f