accessor-style iInv without Hclose

This changes iInv to no longer produce closing view shifts, but instead change the goal, accessor-style. For example, if the goal starts out being WP e @ E {{ v, Q }}, then when opening inv N I it becomes WP e @ (E\N) {{ v, \later I * Q }}. The transformation is performed by a new InvOpener typeclass.

I ported existing proofs in this repo to work with the new tactic. The new tactic is slightly weaker, so not all proofs could be ported: If the goal is accessor-like, one has to use the underlying invariant accessor (inv_open). That's only minimally more involved than using the old iInv, and if we ever have accessors as a notion in their own right then they will also support the new iInv. Notably, all the proofs in the actual examples were easily ported, and they now do not have "Hclose" cluttering the context any more.

One interesting question is whether one can make a connection between InvOpener and ElimModal, but I found no good way to do that. Also we could bikeshed over the name InvOpener, the class is kind-of more general than that and maybe should have "Accessor" somewhere in its name. AccessorElim? (EDIT: I went for AccElim for now.)

Fixes #94 (closed)

This includes !142 (merged), so that one should probably get reviewed and merged first.

Cc @robbertkrebbers @jtassaro who introduced ElimInv