(10steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hel
nuprl
1
1
2
1.
'a
: S
2.
'a
List
3.
u
:
'a
4.
v
:
'a
List
5.
n
:
.
n
<||
v
||
el(
n
,
v
) =
v
[
n
]
6.
n
:
7.
n
<||
v
||+1
8. (
n
=
0) = true
n
<||cons(
u
;
v
)||
By:
RW HNC -1
Generated subgoal:
1
8.
n
= 0
n
<||cons(
u
;
v
)||
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
n:
. n<||v|| 
el(n,v) = v[n]
0) = true
n<||cons(u; v)||
