This better seals off their definition. Although it did not give
much of a speedup, I think it is conceptually nicer.

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.

With Set Printing All, these notations make me loose overview entirely.

barrier: strive for consistency between barrierGF and the inGF assumptions; also change some instance names

This reverts commit 7266d16b

And now the part that I forgot to commit.

I made the list of iFunctors monomorphic to avoid having to deal with
universe polymorphism, that is still somewhat flaky.

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.

The non applied one should be only parsing.