(10steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list
append
singleton
ind
1
1.
T
: Type
2.
Q
: (
T
List)
Prop
3.
Q
(nil)
4.
ys
:
T
List,
x
:
T
.
Q
(
ys
)
Q
(
ys
@ [
x
])
zs
:
T
List.
Q
(
zs
)
By:
Assert (
n
:
,
l
:
T
List. ||
l
|| =
n
Q
(
l
))
Generated subgoals:
1
n
:
,
l
:
T
List. ||
l
|| =
n
Q
(
l
)
7
steps
2
5.
n
:
,
l
:
T
List. ||
l
|| =
n
Q
(
l
)
zs
:
T
List.
Q
(
zs
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc