(3steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
es-ble
wf
es
:ES,
e
,
e'
:E. es-ble{i:l}(
es
;
e
;
e'
)
By:
Auto THEN Unfold `es-ble` 0 THEN GenConclAtAddr [2;1;1;1;1] THEN Thin -1
Generated subgoal:
1
1.
es
: ES
2.
e
: E
3.
e'
: E
4.
v
:
the_es
:ES,
e'
,
e
:E. Dec(
e
e'
)
InjCase(
v
(
es
,
e'
,
e
);
x
. true
, false
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
es:ES, e,e':E. es-ble{i:l}(es;e;e') 
es:ES, e,e':E. es-ble{i:l}(es;e;e') the_es:ES, e',e:E. Dec(e 
e' )
InjCase(v(es,e',e); x. true
, false) 
