(6steps 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:
counting
is
unique
1
1.
A
: Type
2.
m
:
3.
k
:
4.
A
~
m
5.
A
~
k
m
=
k
By:
x
,
y
:
. (
x
~
y
)
x
y
Asserted
Generated subgoals:
1
6.
x
:
7.
y
:
8.
x
~
y
x
y
3
steps
2
6.
x
,
y
:
. (
x
~
y
)
x
y
m
=
k
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc