(8steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hel
wf
1
1
1.
'a
: S
(
n
:
.
l
:
'a
List. el(
n
,
l
))
(
hlist(
'a
)
'a
)
By:
RepeatFor 2 Analyze THEN CAuto
Generated subgoal:
1
2.
n
:
3.
l
: hlist(
'a
)
el(
n
,
l
)
'a
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
(
n:
. l:'a List. el(n,l)) 
( 
hlist('a) 'a) (n:. l:'a List. el(n,l)) ( hlist('a) 'a)
el(n,l) 'a
