Consistent variable and hypothesis naming
Changes in the implementation and in the available hints can cause changes in variable names, which is unwanted. Different versions of Iris have also sometimes caused different hypotheses names, also unwanted.
Idea to get consistent hypotheses names: don't use the IPM environment, instead use a custom list environment, and change back to the IPM env after a tactic finishes.
Idea to get consistent variable names: look at how IPM does it for foralls. Otherwise try typeclasses to generate 'good' default names..?