(3steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub not infinite 1 1
1. k : 
2. Finite(k)
3. Infinite(k)
  False
By: FwdThru: Thm*  Infinite(A)  Finite(A) on [ Hyp:-1 ]

Generated subgoals:

None

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

(3steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc