(8steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
pigeon
hole
1
1
1
1
1.
m
:
2.
k
:
3.
f
:
m
k
4.
k
<
m
5. Inj(
m
;
;
f
)
m
k
By:
BackThru:
Thm*
(
f
:(
m
k
). Inj(
m
;
k
;
f
))
m
k
Generated subgoal:
1
f
:(
m
k
). Inj(
m
;
k
;
f
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
m
k
m; 
; f)
m
k
mk
m; ; f)
mk
f:(mk). Inj(m; k; f)) 
mk f:(mk). Inj(m; k; f)
