(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
  (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D))
By: 2 Times Analyze THEN Witness1: D

Generated subgoal:

1 1. D : Type
2. Finite(D)  Unbounded(D)
  (D)  (D)
10 steps

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

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