(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.
'a
: S
el
(
hlist(
'a
)
'a
)
By:
RW (TopC EtaExpHRecC) 0
Generated subgoal:
1
(
n
:
.
l
:
'a
List. el(
n
,
l
))
(
hlist(
'a
)
'a
)
6
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
el 
(
hlist('a) 'a) el ( hlist('a) 'a) (
n:. l:'a List. el(n,l)) ( hlist('a) 'a)
