(5steps 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 comp1

  m,k:f:((m+1)(k+1)).
  Inj((m+1); (k+1); f)
  
  (i:mf(i) = k  (Replace value k by f(m) in f)(i) = f(m k)


By: Auto


Generated subgoal:

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
  (Replace value k by f(m) in f)(i) = f(m k

4 steps

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

(5steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc