GitLab

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

Show that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-condition

New atomic updates: defined as a fixed point with existential quantifier; intro lemma using class of Laterable assertions

There's a very low risk of these conflicting with Coq's standard library

- Make `flöb_pre` and `flöb` local to the proof.
- The metavariables `Ψ` are used for predicates, so use a `Q` here.

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

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.

Fixes #156

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

Fixes #177

Fixes #176