(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.
m
:
2.
k
:
3.
f
:
(
m
+1)
(
k
+1)
4. Inj(
(
m
+1);
(
k
+1);
f
)
5.
i
:
m
if
f
(
i
)=
k
f
(
m
) else
f
(
i
) fi
k
By:
EqIntCases 0
Generated subgoal:
1
6.
f
(
i
) =
k
f
(
m
)
k
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
if f(i)=
k
f(m) else f(i) fi 
