An example and a counterexample at the same time: Dowker's Theorem. (See, for example, this question: What are the applications of Dowker's theorem?)
Dowker's theorem asserts that (the geometric realizations of) two simplicial complexes, $K$ and $L$, associated to a binary relation $R\subseteq X\times Y$ are homotopy equivalent. As I understand it, the proof of this equivalence requires a choice of ordering of the simplices; but the particular ordering used is not relevant, i.e., any total order can be used. (Please correct me if I'm wrong here!)
This is either an example, or a counterexample, depending how one looks at it. On the one hand, the equivalence of homotopy type between $K$ and $L$, as a proposition which is true, does not depend on the choice of ordering; on the other hand, in order to get a particular homotopy equivalence between $K$ and $L$, a choice of ordering is necessary: the equivalence provided by Dowker's theorem is not natural.