(4steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hinfinity
ax
1
f
:(
). one_one(
;
;
f
) &
onto(
;
;
f
)
By:
((DTerm (
x
.
x
+1) 0) THEN (Unab [`one_one`;`onto`])) THEN Simp THEN StrongAuto
Generated subgoal:
1
(
y
:
.
x
:
.
y
=
x
+1
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
f:(
). one_one(;;f) & 
onto(;;f) f:(). one_one(;;f) & onto(;;f)
x.x+1) 0) THEN (Unab [`one_one`;`onto`])) THEN Simp THEN StrongAuto (
y:. x:. y = x+1 
)
