Tactic(s) for "freshness" of names

[mtoohey31]

There should be an easier way to require that identifiers must be fresh with respect to different things, since doing it manually is annoying.

There are two ways such variables may be introduced, and this should ideally support both:

• When you're just picking something random that will be introduced in/used to specialize something else.
• When showing a hypothesis which uses co-finite quantification.

At the very least the tactic(s) should support generation of freshness hypotheses at the creation site of the identifier. More optimally though, if it's possible to use mvars so that freshness conditions can just be created with another tactic at their use sites, that would be even better. Even if the latter is possible though, the former may also be necessary in some cases (such as potentially those involving induction).