(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
Any way of counting a finite class produces the same number.

At: counting is unique

  A:Type, m,k:. (A ~ m)  (A ~ k)  m = k
By: Auto

Generated subgoal:

1 1. A : Type
2. m : 
3. k : 
4. A ~ m
5. A ~ k
  m = k
5 steps

About:
natural_numberuniverseequalimpliesall
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