I meant it in the sense that I assume GP meant it, i.e., the index of an element in an ordered set is an integer corresponding to its position in that set, starting at 0 or 1 for the first element (depending on your indexing scheme of choice).

Does the axiom of choice let you repeatedly pick the same real numbers in the same order out of a set? Or do you need uncountably infinite storage to keep your list of indexes?

That's an interesting question, but kind of hard to answer. Programming is inherently constructive so approaching a non-constructive proof as a programming problem tends to be problematic.

I don't think you run into any problems if you let the axiom of choice pick the same numbers every time. It would be a bit problematic if you were to add that as an extra axiom (suddenly every proof let x,y in X then ... therefore x=y would become trivial).