(5steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
delete
fenum
value
comp1
1
1
1.
m
:
2.
k
:
3.
f
:
(
m
+1)
(
k
+1)
4. Inj(
(
m
+1);
(
k
+1);
f
)
5.
i
:
m
6.
f
(
i
) =
k
f
(
m
) =
f
(
m
)
k
By:
f
(
m
) =
k
Asserted
Generated subgoal:
1
f
(
m
) =
k
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
f(m) = f(m) 
f(m) = k 
Asserted
