This is in preparation for coq/coq#9274.

This lemma is similar to `later_ownM`.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.

Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.

With a pretty proof by Robbert

The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.

Fixes #193

Thanks to @dfrumin.

This version allows one to either close or cancel the invariant after opening it.

This follows the proof at https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem

If the accessor introduces a binder, the first Coq-level intro pattern of `iInv`
is used for that binder unless the type of the binder is unit, in which case
`iInv` removes it completely.  Binders on the closing view shift are not (yet)
supported as they are harder to smoothly eliminate in the unit case.

New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hclose