(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: absurd nonfin imp unb inf 1 1 1 1
1. D : Type
2. n : 
3. (D) ~ n
4. D
  Infinite(n)
By: FwdThru: Thm*  (A ~ B)  Infinite(A)  Infinite(B) on [ (D) ~ n ]

Generated subgoal:

1   Infinite(D)
3 steps

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

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