mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm* m,n,k:f:(nm), g:(km).
Thm* increasing(f;n)
Thm* 
Thm* increasing(g;k)
Thm* 
Thm* (i:m. (j:ni = f(j))  (j:ki = g(j)))
Thm* 
Thm* (j1:nj2:kf(j1) = g(j2))  m = n+k  
[disjoint_increasing_onto]
cites the following:
1Thm* k,m:. (f:(km). Inj(kmf))  km[injection_le]
1Thm* k,m:f:(km). increasing(f;k Inj(kmf)[increasing_inj]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb nat Sections MarkB generic Doc