PrintForm
Definitions
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
htl
wd
'a
:S. all(
t
:hlist(
'a
). all(
h
:
'a
. equal(tl(cons(
h
,
t
)),
t
)))
By:
HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
list
2
Sections
HOLlib
Doc
'a:S. all(
t:hlist('a). all(h:'a. equal(tl(cons(h,t)),t))) 'a:S. all(t:hlist('a). all(h:'a. equal(tl(cons(h,t)),t)))
