(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value wf 1 1 1

1. m : 
2. k : 
3. f : (m+1)(k+1)
4. Inj((m+1); (k+1); f)
5. i : m
6. f(i) = k
  f(m k


By: f(m) = k    Asserted


Generated subgoal:

1   f(m) = k
3 steps

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

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc