(46steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
num
iso
2
1
2
1
1
1
1
1.
f
:
2. one_one(
;
;
f
)
3.
onto(
;
;
f
)
one_one(
;
;
x
:
.
f
(
x
))
By:
Subst ((
x
:
.
f
(
x
)) =
f
) 0 THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))
Generated subgoal:
1
(
x
:
.
f
(
x
)) =
f
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(46steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
;;f)
onto(;;f)
one_one(;;
x:. f(x))
;;f)
onto(;;f)
one_one(;;x:. f(x))x:. f(x)) = f) 0 THEN StrongAuto
(x:. f(x)) = f
