(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 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)
  mn+k


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


Generated subgoal:

1   f:(m(n+k)). Inj(m(n+k); f)
10 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