(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
1
1
1.
es
: ES
2.
e
: E
3.
e'
: E
4.
the_es
:ES
e'
,
e
:E
Dec(
e
e'
)
5.
v1
: Dec(
e
e'
)
InjCase(
v1
;
x
. true
, false
)
e
e'
By:
Analyze -1 THEN Reduce 0
Generated subgoal:
1
5.
e
e'
6.
e
e'
False
1
step
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
e',e:E
e' )
InjCase(v1; x. true
, false
e 
e 
