(13steps total)
PrintForm
Definitions
Lemmas
mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l
member
decomp
2
1.
T
: Type
2.
T
List
3.
u
:
T
4.
v
:
T
List
5.
x
:
T
. (
x
v
)
(
l1
,
l2
:
T
List.
v
= (
l1
@ [
x
] @
l2
))
6.
x
:
T
7.
x
=
u
(
x
v
)
l1
,
l2
:
T
List. [
u
/
v
] = (
l1
@ [
x
] @
l2
)
By:
Analyze -1
Generated subgoals:
1
7.
x
=
u
l1
,
l2
:
T
List. [
u
/
v
] = (
l1
@ [
x
] @
l2
)
1
step
2
7. (
x
v
)
l1
,
l2
:
T
List. [
u
/
v
] = (
l1
@ [
x
] @
l2
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
Lemmas
mb
event
system
1
Sections
EventSystems
Doc