(5steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
member-es-interval
es
:ES,
e
,
e'
,
ev
:E. (
ev
[
e
,
e'
])
e
ev
&
ev
e'
By:
UnivCD
Generated subgoal:
1
1.
es
: ES
2.
e
: E
3.
e'
: E
4.
ev
: E
(
ev
[
e
,
e'
])
e
ev
&
ev
e'
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc
es:ES, e,e',ev:E. (ev 
[e, e']) 
e 
ev & ev e' es:ES, e,e',ev:E. (ev [e, e']) e ev & ev e' (ev [e, e']) e ev & ev e' 
