(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