(6steps total)
Remark
PfGloss
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite
inj
counter
example
1
1.
m
:
2.
f
:
m
3.
Inj(
m
;
;
f
)
x
:
m
,
y
:
x
.
f
(
x
) =
f
(
y
)
By:
Decide:
x
:
m
,
y
:
x
.
f
(
x
) =
f
(
y
)
THEN Analyze3
Generated subgoal:
1
4.
(
x
:
m
,
y
:
x
.
f
(
x
) =
f
(
y
))
Inj(
m
;
;
f
)
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
Remark
PfGloss
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
Inj(
x:
