(4steps 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:
assert-es-ble
es
:ES,
e
,
e'
:E. es-ble{i:l}(
es
;
e
;
e'
)
e
e'
By:
UnivCD THEN Unfold `es-ble` 0 THEN GenConclAtAddr [1;1;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
)
e
e'
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
es:ES, e,e':E. es-ble{i:l}(es;e;e') 
e 
e' es:ES, e,e':E. es-ble{i:l}(es;e;e') e e' the_es:ES, e',e:E. Dec(e e' )
InjCase(v(es,e',e); x. true
, false) e e' 
