PrintForm
Definitions
Lemmas
hol
one
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
axiom
2
'a
:S,
e
:
'a
.
(
fn
:(Unit
'a
).
fn
(
) =
e
)
& (
fn
,
y
:(Unit
'a
).
fn
(
) =
e
&
y
(
) =
e
fn
=
y
)
By:
RewriteOfThm
Thm*
'a
:S. all(
e
:
'a
. exists_unique(
fn
:hone
'a
. equal(
fn
(one_el),
e
)))
HNC
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
one
Sections
HOLlib
Doc