This introduces n hypotheses and destructs the nth one.

be the same as .

This is a fairly intrusive change, but at least makes notations more
consistent, and often shorter because fewer parentheses are needed. Note
that viewshifts already had the same precedence as →.

It used to be: (P ={E}=> Q) := (True ⊢ (P → |={E}=> Q))
Now it is: (P ={E}=> Q) := (P ⊢ |={E}=> Q)

Based on an idea and WIP commits of J-H. Jourdan: the core of a CMRA
A is now a partial function A → option A.

TODO: define sum CMRA
TODO: remove one shot CMRA and define it in terms of sum

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.

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.

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

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

* Use sig instead of sigT: the proof is a Prop after all
* Tweak implicit arguments
* Shorten proof of sigma

I am now also using reification to obtain the indexes corresponding to
the stuff we want to cancel instead of relying on matching using Ltac.

And now the part that I forgot to commit.

Also, give all these global functors the suffix GF to avoid shadowing
such as we had with authF.

And add some type annotations for clarity.

I added a new typeclass "inGF" to witness that a particular *functor* is part of \Sigma. inG, in contrast, witnesses a particular *CMRA* to be in there, after applying the functor to "\later iProp".
inGF can be inferred if that functor is consed to the head of \Sigma, and it is preserved by consing a new functor to \Sigma. This is not the case for inG since the recursive occurence of \Sigma also changes.
For evry construction (auth, sts, saved_prop), there is an instance infering the respective authG, stsG, savedPropG from an inGF. There is also a global inG_inGF, but Coq is unable to use it.

I tried to instead have *only* inGF, since having both typeclasses seemed weird. However, then the actual type that e.g. "own" is about is the result of applying a functor, and Coq entirely fails to infer anything.

I had to add a few type annotations in heap.v, because Coq tried to use the "authG_inGF" instance before the A got fixed, and ended up looping and expanding endlessly on that proof of timelessness.
This does not seem entirely unreasonable, I was honestly surprised Coq was able to infer the types previously.