PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
existse-at
wf
es
:ES,
i
:Id,
P
:({
e
:E| loc(
e
) =
i
Id }
Prop).
e
@
i
.
P
(
e
)
Prop
By:
Unfold `existse-at` 0 THEN Unfold `and` 0 THEN Fold `cand` 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
es:ES, i:Id, P:({e:E| loc(e) = i 
Id }
Prop). 
e@i.P(e) Prop es:ES, i:Id, P:({e:E| loc(e) = i Id }Prop). e@i.P(e) Prop
