(7steps 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
wf
1
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
)
k
By:
f
(
m
) =
k
Asserted
Generated subgoal:
1
f
(
m
) =
k
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc