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

rename : affinely_persistently -> intuitionistically. Add lemma about monpred_at and intuitionistically.

Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.

The closing view shift's LHS mask is now universally quantified, which
makes it easier to execute the closing view shift.

This is a substitute for !136.

This is backwards-compatible; it desugars to a normal application on previous versions

Based on an earlier MR by @jung.

This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.

As suggested by @jjourdan, and proved in the ordered RA model by @amintimany.

This should solve the paradox in #149.

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type."

This reverts commit fa897ff5.