Get rid of star specialization pattern.

As I mentioned in #62 (closed), I would like to get rid of the specialization pattern * and instead instantiate all universal quantifiers automatically when applying or destructing. This merge request implements that.

There is however one open issue: when destructing a persistent hypothesis we have to decide when to keep the original and when to remove it. To illustrate why, consider having the following hypothesis in the persistent context:

H : ∀ x, P x ∨ Q x

Clearly, when doing an iDestruct we would like to keep the original. After all, we may want to instantiate it with different values for x. However, when having a disjunction that is not universally quantified, it is safe to remove the original because it does not lead to loss of information.

The current heuristic for determining whether to keep a hypothesis is rather stupid: it only copies when variables are explicitly instantiated, i.e. when having a non-empty list x1 ... xn in the below.

iDestruct ("H" $! x1 ... xn)

Now that we automatically instantiate universal quantifiers, this heuristic may not be the best idea anymore.

Any ideas for a better heuristic?