For model-automaton product constructions, we would like to add automatically generated labels to the result, so we need a way to ensure that we can get those without clashing with existing labels.