(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: unboundedly imp productively infinite
  A:Type. Infinite(A)  Unbounded(A)
By: Def of Infinite(A) | Unbounded(A) THEN (Def of <Type> inj <Type> ; Id)

Generated subgoal:

1 1. A : Type
2. ( inj A)
3. k : 
  (k inj A)
3 steps

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

(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc