(10steps 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:
es-first-exists
1
1
1.
es
: ES
2. WellFnd{i}(E;
x
,
y
.(
x
<loc
y
))
3.
j
: E
4.
k
:E. (
k
<loc
j
)
(
e
:E. first(
e
) &
e
k
)
5. first(
j
)
e
:E. first(
e
) &
e
j
By:
InstConcl [
j
]
Generated subgoal:
1
j
j
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc
k:E. (k <loc j) 
(
e:E. first(e) & e 
k )
