(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. D : Type
2. Finite(D)  Unbounded(D)
  (D)  (D)
By: Guarding (D) SimilarTo: Hyp:-1

Generated subgoals:

1 2. Finite(D)
  (D)
6 steps
2 2. (D)
3. Unbounded(D)
  D
3 steps

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

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