(10steps 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:
maximal-in-list
1
1
1.
A
: Type
2.
f
:
A
3.
A
List
4.
u
:
A
5. 0<||nil||
(
a
nil.(
x
nil.
f
(
x
)
f
(
a
)))
6. 0<||nil||+1
(
a
[
u
].(
x
[
u
].
f
(
x
)
f
(
a
)))
By:
Unfold `l_exists` 0 THEN InstConcl [
u
]
Generated subgoals:
1
(
u
[
u
])
1
step
2
(
x
[
u
].
f
(
x
)
f
(
u
))
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
1
Sections
EventSystems
Doc
(
a
nil.(
x
f(a)))
(
