PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map
append
2
'a
,
'b
:S,
f
:(
'a
'b
),
l1
,
l2
:
'a
List. map(
f
;
l1
@
l2
) = (map(
f
;
l1
) @ map(
f
;
l2
))
By:
RewriteOfThm Thm:
hmap
append
2
(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,'b:S, f:('a
'b), l1,l2:'a List. map(f;l1 @ l2) = (map(f;l1) @ map(f;l2))
