(10steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value is inj 1 1
1. m : 
2. k : 
3. f : (m+1)(k+1)
4. Inj((m+1); (k+1); f)
5. a1 : m
6. a2 : m
7. (Replace value k by f(m) in f)(a1) = (Replace value k by f(m) in f)(a2)
  a1 = a2
By: Decide: f(a1) = k   THEN Decide: f(a2) = k  

Generated subgoals:

1 8. f(a1) = k
9. f(a2) = k
  a1 = a2
1 step
2 8. f(a1) = k
9. f(a2) = k
  a1 = a2
2 steps
3 8. f(a1) = k
9. f(a2) = k
  a1 = a2
2 steps
4 8. f(a1) = k
9. f(a2) = k
  a1 = a2
2 steps

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

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