(2steps total)
PrintForm
Definitions
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hhd
wd
'a
:S. all(
t
:hlist(
'a
). all(
h
:
'a
. equal(hd(cons(
h
,
t
)),
h
)))
By:
HN THEN Try (Complete Auto)
Generated subgoal:
1
1.
'a
: S
2.
t
: hlist(
'a
)
3.
h
:
'a
mt(cons(
h
;
t
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
hol
list
2
Sections
HOLlib
Doc
'a:S. all(
t:hlist('a). all(h:'a. equal(hd(cons(h,t)),h))) 'a:S. all(t:hlist('a). all(h:'a. equal(hd(cons(h,t)),h))) 
mt(cons(h; t))
