PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dedekind imp nonfin
  A:Type. Dedekind-Infinite(A)  Finite(A)
By: BackChain: 
Thm*  Dedekind-Infinite(A)  Infinite(A) |
Thm*  Infinite(A)  Finite(A)

Generated subgoals:

None

About:
universeimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc