n,m:, f:(nm). Inj(n; m; f)  nm

1

1. n :  2. m :  3. f : nm 4. Inj(n; m; f) 5. p : m( List) 6. sum(||p(j)|| | j < m) = n 7. j:m, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y] 8. j:m, x:||p(j)||. (p(j))[x]<n & f((p(j))[x]) = j   nm

9 steps

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