PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
null
char
'a
:S. True & (
h
:
'a
,
t
:
'a
List. True)
By:
RewriteOfThm
Thm*
'a
:S. and(null(nil),all(
h
:
'a
. all(
t
:hlist(
'a
). not(null(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. True & (h:'a, t:'a List. True) 'a:S. True & (h:'a, t:'a List. True)'a:S. and(null(nil),all(
h:'a. all(t:hlist('a). not(null(cons(h,t))))))
