PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
nil
cons
'a
:S,
t
:
'a
List,
h
:
'a
.
nil = cons(
h
;
t
)
By:
RewriteOfThm
Thm*
'a
:S. all(
t
:hlist(
'a
). all(
h
:
'a
. not(equal(nil,cons(
h
,
t
)))))
(SimpsetC [`hol_to_nuprl`;`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
'a:S, t:'a List, h:'a. 
nil = cons(h; t) 'a:S, t:'a List, h:'a. nil = cons(h; t)'a:S. all(
t:hlist('a). all(h:'a. not(equal(nil,cons(h,t)))))
