* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors

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

`sed -i 's/frag_auth_op/frac_auth_frag_op/g' $(find -name "*.v")`

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

  Also, remove the inconsistency that `wp_expr_eval` succeeds on a goal
  that is not a WP.

We now use the `Maybe` prefix as also used for `Frame`: it indicates
whether progress has been made by stripping of a later or not.

For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.

This is to make sure that e.g. `//` in `iEval (rewrite .. // ..)` does
not immediately close the goal by reflexivity.