That is, given a non-injective assigment of integers to a finite collection we can find two objects (with the second objects y preceding the first value x) that are assigned the same value.
This reduces to showing the contrapositive, namely

(x:m, y:x. f(x) = f(y)) Inj(m; ; f)

(computationally, since there are only finitely many choices for x and y in the specified domain, one could just exhaustively try them all and see if there is a pair whose assignments by f agree).
So assuming that