(2steps total)
PrintForm
Definitions
mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
es-le-loc
es
:ES,
e
,
e'
:E.
e
e'
loc(
e
) = loc(
e'
)
Id
By:
Unfold `es-le` 0 THEN Unfold `es-locl` 0 THEN Analyze -1
Generated subgoal:
1
1.
es
: ES
2.
e
: E
3.
e'
: E
4.
e
=
e'
loc(
e
) = loc(
e'
)
Id
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
2
Sections
EventSystems
Doc
es:ES, e,e':E. e 
e' 
loc(e) = loc(e') 
Id es:ES, e,e':E. e e' loc(e) = loc(e') Id loc(e) = loc(e') Id
