(22steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: disjoint increasing onto 1 2 1

1. m : 
2. n : 
3. k : 
4. f : nm
5. g : km
6. increasing(f;n)
7. increasing(g;k)
8. i:m. (j:ni = f(j))  (j:ki = g(j))
9. j1:nj2:kf(j1) = g(j2)
10. mn+k
  n+km


By: BackThru Thm* k,m:. (f:(km). Inj(kmf))  km


Generated subgoal:

1   f:((n+k)m). Inj((n+k); mf)
6 steps

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

(22steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc