PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list
not
eq
'a
:S,
l1
,
l2
:
'a
List.
l1
=
l2
(
h1
,
h2
:
'a
.
cons(
h1
;
l1
) = cons(
h2
;
l2
))
By:
RewriteOfThm Thm:
hlist
not
eq
(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, l1,l2:'a List. 
l1 = l2 
(
