PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
cons
11
'a
:S,
h
:
'a
,
t
:
'a
List,
h'
:
'a
,
t'
:
'a
List.
cons(
h
;
t
) = cons(
h'
;
t'
)
h
=
h'
&
t
=
t'
By:
RewriteOfThm Thm:
hcons
11
(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, h:'a, t:'a List, h':'a, t':'a List.
cons(h; t) = cons(h'; t') 
h = h' & t = t'
