Currently the translator renames all variables as vN for numbers N that are kept globally distinct with a counter. It could make more readable code if it used the variable names from the shallow embedding and only introduced a number if necessary to avoid shadowing.