PrintForm
Definitions
Lemmas
mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
es-E
equal
the_es
:ES,
e
,
e'
:E. Dec(
e
=
e'
)
By:
Auto THEN RWO
Thm*
the_es
:ES,
e
,
e'
:E.
e
=
e'
e
=
e'
0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
event
system
2
Sections
EventSystems
Doc
the_es:ES, e,e':E. Dec(e = e') the_es:ES, e,e':E. Dec(e = e')the_es:ES, e,e':E. e = e' 
e = e' 0
