(9steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
listify
length
T
:Type,
m
,
n
:
,
f
:({
m
..
n
}
T
).
n
<
m
||
f
{
m
..
n
}|| =
n
-
m
By:
UnivCD
Generated subgoal:
1
1.
T
: Type
2.
m
:
3.
n
:
4.
f
: {
m
..
n
}
T
n
<
m
||
f
{
m
..
n
}|| =
n
-
m
8
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
T:Type, m,n:
, f:({m..n
}
T). n<m 
||f{m..n}|| = n-m T:Type, m,n:, f:({m..n}T). n<m ||f{m..n}|| = n-m
}T
n<m ||f{m..n}|| = n-m
