(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
'a
:S,
n
:
,
l
:
'a
List.
n
<||
l
||
el(
n
,
l
) =
l
[
n
]
By:
RepeatMFor 3 (Try (Analyze 0)) THEN CAuto
Generated subgoal:
1
1.
'a
: S
2.
n
:
3.
l
:
'a
List
4.
n
<||
l
||
el(
n
,
l
) =
l
[
n
]
9
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
'a:S, n:
, l:'a List. n<||l|| 
el(n,l) = l[n] 'a:S, n:, l:'a List. n<||l|| el(n,l) = l[n]
el(n,l) = l[n]
