(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
1. D : Type
2. n : 
3. (D) ~ n
4. D
  Infinite(D)
By: New:d Analyze4 THEN Witness: i.<i,d>

Generated subgoal:

1 4. d : D
  Inj(; D; i.<i,d>)
2 steps

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

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