Thm* n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j) phole_lemma
Thm* n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j) phole_aux
In prior sections: int 1 int 2
n:{1...}, m:{n+1...}, f:(
m
n). 
i,j:m. i < j & f(i) = f(j) phole_lemma
| i
j }
n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j) phole_lemma
n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j) phole_aux