IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
pigeon-hole11 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 sum(||p(j)|| | j < m)1m
By:
BackThru Thm*k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)bk