Add 'equiv' to autocompletion of tactics
Add %name directive for naming hints in editing.

Gives a list of preferred names for a particular type family. If none
are available when generating names, just try adding a digit to each
in turn.

Also generate appropriate names for function arguments, and have a new
set of invented names when nothing else is available.