Invent names when case splitting

Although the choices are not always very good, this is useful because
it means if any names are unified, you get told about it directly.

Names are taken from binder names, and a digit added if they are not
unique.