mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
the_es
:ES,
e
,
e'
:E. Dec(
e
=
e'
)
[decidable__es-E_equal]
cites the following:
Thm*
the_es
:ES,
e
,
e'
:E.
e
=
e'
e
=
e'
[assert-es-eq-E]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
2
Sections
EventSystems
Doc
the_es:ES, e,e':E. Dec(e = e')the_es:ES, e,e':E. e = e' 
e = e'the_es:ES, e,e':E. Dec(e = e')the_es:ES, e,e':E. e = e' e = e'