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.

this makes it slightlymore annoying to use because we have to elliminate the box. one more reason to have a proof mode ;-)

* Put level of the triple at 20, so we can write things like
  ▷ {{ P }} e @ E {{ Φ }} without parentheses.
* Use high levels for P, e and Φ.
* Allow @ E to be omitted in case E = ⊤.

This avoids ambiguity with P and Q that we were using before for both
uPreds/iProps and indexed uPreds/iProps.

simplify_equality        => simplify_eq
simplify_equality'       => simplify_eq/=
simplify_map_equality    => simplify_map_eq
simplify_map_equality'   => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality   => simplify_list_eq
f_equal'                 => f_equal/=

The /= suffixes (meaning: do simpl) are inspired by ssreflect.