(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.
'a
: S
2.
n
:
3.
l
:
'a
List
4.
n
<||
l
||
el(
n
,
l
) =
l
[
n
]
By:
MoveToConcl 2 THEN Last ListInd THEN Simp THEN StrongAuto
Generated subgoal:
1
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
el(
n
,cons(
u
;
v
)) = cons(
u
;
v
)[
n
]
8
steps
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
el(n,l) = l[n]
el(n,l) = l[n]
n:. n<||v|| 
el(n,v) = v[n]
el(n,cons(u; v)) = cons(u; v)[n]
