(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
1.
'a
: S
2.
n
:
3.
l
: hlist(
'a
)
el(
n
,
l
)
'a
By:
MoveToConcl 3 THEN NInd 2 THEN CAuto
Generated subgoals:
1
2.
l
: hlist(
'a
)
el(0,
l
)
'a
1
step
2
2.
n
:
3. 0<
n
4.
l
:hlist(
'a
). el(
n
-1,
l
)
'a
5.
l
: hlist(
'a
)
el(
n
,
l
)
'a
3
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(n,l) 
'a
el(n,l) 'a el(0,l) 'a
l:hlist('a). el(n-1,l) 'a
el(n,l) 'a
