(6steps total) Remark PfGloss PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite inj counter example 1 1
1. m : 
2. f : m
3. Inj(m; ; f)
4. (x:m, y:x. f(x) = f(y))
  Inj(m; ; f)
By: Analyze

Generated subgoal:

1 5. a1 : m
6. a2 : m
7. f(a1) = f(a2)
  a1 = a2
3 steps

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

(6steps total) Remark PfGloss PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc