Strategy for inventing fresh names

[hrutvik]

Currently, we use an unusual strategy for inventing fresh names: we append sequential numbers to a base name in the hope we produce something fresh, and if we fail we simply create a name longer than any we know. This is partly to ensure the definition is translatable: we can't require map_ok to hold of the set of known variable names.

An alternative approach does not require map_ok, as long as it can override the comparison function used in the map. This issue is about fleshing out this approach to produce nicer variable names, getting it translated, and replacing the existing unusual approach.