(3steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
select
tl
2
1.
A
: Type
2.
A
List
3.
u
:
A
4.
v
:
A
List
5.
n
:
(||
v
||+1-1)
v
[
n
] = (
u
.
v
)[(
n
+1)]
By:
RWO
Thm*
a
:
T
,
as
:
T
List,
i
:
. 0<
i
i
||
as
||
(
a
.
as
)[
i
] =
as
[(
i
-1)] 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
(||v||+1-1)
v[n] = (u.v)[(n+1)]
a:T, as:T List, i:
. 0<i 
i
||as|| 
