mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
the_w
:World,
e
:E. first(
e
)
[w-first_wf]
cites the following:
Thm*
the_w
:World,
i
:Id,
t
:
. first(<
i
,
t
>)
[w-first-aux]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
3
Sections
EventSystems
Doc
the_w:World, e:E. first(e) 
the_w:World, i:Id, t:
. first(<i,t>) the_w:World, e:E. first(e) the_w:World, i:Id, t:. first(<i,t>)