(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 1 1 1 1
1. D : Type
2. n : 
3. (D) ~ n
4. d : D
  Inj(; D; i.<i,d>)
By: Analyze THEN Reduce Concl

Generated subgoal:

1 5. a1 : 
6. a2 : 
7. <a1,d> = <a2,d>
  a1 = a2
1 step

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

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