IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
pigeon-hole1 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