Rationale: to make the code closer to what is on paper, I want the notations
to look like quantifiers, i.e. have a binder built-in. I thus introduced the
following notations:

  [★ map] k ↦ x ∈ m, P
  [★ set] x ∈ X, P

The good thing - contrary to the notations that we had before that required an
explicit lambda - is that type annotations of k and x are now not printed
making goals much easier to read.

To do so, we have introduced the specialization patterns:

  =>[H1 .. Hn] and =>[-H1 .. Hn]

That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.

Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).

TODO: change the name of these specialization patterns to reflect this
generality.

Changes:
- We no longer have a different syntax for specializing a term H : P -★ Q whose
  range P or domain Q is persistent. There is just one syntax, and the system
  automatically determines whether either P or Q is persistent.
- While specializing a term, always modalities are automatically stripped. This
  gets rid of the specialization pattern !.
- Make the syntax of specialization patterns more consistent. The syntax for
  generating a goal is [goal_spec] where goal_spec is one of the following:

    H1 .. Hn : generate a goal using hypotheses H1 .. Hn
   -H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn
           # : generate a goal for the premise in which all hypotheses can be
               used. This is only allowed when specializing H : P -★ Q where
               either P or Q is persistent.
           % : generate a goal for a pure premise.

iSpecialize and iDestruct.

These tactics now all take an iTrm, which is a tuple consisting of
a.) a lemma or name of a hypotheses b.) arguments to instantiate
c.) a specialization pattern.

These tactics are superfluous:
- iPure H as pat => iDestruct H as pat
- iPersistent H => iSpecialize H "!"

- It can now also frame under later.
- Better treatment of evars, it now won't end up in loops whenever the goal
  involves sub-formulas ?P and it trying to apply all framing rules eagerly.
- It no longer delta expands while framing.
- Better clean up of True sub-formulas after a successful frame. For example,
  framing "P" in "▷ ▷ P ★ Q" yields just "Q" instead of "▷ True ★ Q" or so.

This gets rid of the (ambiguous) notation %l, because we can declare
LitLoc as a coercion. It also shortens the code.

This reverts commit 3cc38ff6.

The reverted pure hypotheses and variables appear in the wrong order.

Since strip_later is doing a good job stripping laters in the conclusion,
these tactics are thus no longer needed. Also, wp_finish now properly
converts the result in a primitive viewshift in case it is not a weakestpre.

Thanks to Amin Timany for the suggestion.

Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.

Since functor instances are just used as combinators, there is really
no need for functors that are not contractive.

make the global functor stuff in the various constructions more uniform; change it such that barrier/proof does not have to repeat the functors it needs

add a version of [cancel] that works with goals of the form [_ |- pvs _]; and use that for the barrier proof

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.