(13steps 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:
firstn
is
iseg
1
1
1
1
1
1.
T
: Type
2.
T
List
3.
l
:
T
List
||firstn(0;
l
)|| = 0
By:
BackThru
Thm*
as
:
A
List,
n
:{0...||
as
||}. ||firstn(
n
;
as
)|| =
n
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
||firstn(0;l)|| = 0 
||firstn(0;l)|| = 0 
as:A List, n:{0...||as||}. ||firstn(n;as)|| = n 
