(22steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: negnegelim imp notfin imp unb inf
  (P:Prop. P  P)  (A:Type. Finite(A)  Unbounded(A))
By: Def of Finite(A) | Unbounded(A)

Generated subgoal:

1 1. P:Prop. P  P
2. A : Type
3. (n:. A ~ n)
4. k : 
  (k inj A)
21 steps

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

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