iInv without Hclose
I've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv.
Particularly, I suggest that we get rid of the last parameter of iInv (the name of the "Hclose"), and instead have it add that as an obligation to the postcondition. So, if the goal starts out being WP e {{ v, Q }}, then when opening inv N I it becomes WP e {{ v, \later I * Q }}. Similar things happen when the goal is a view shift.
@robbertkrebbers @jjourdan what do you think? How hard would it be to implement this? We'd probably want a new typeclass generalizing things that can be in the goal when doing iInv. I fear that typeclass will be much like the infamous "frame shift assertions"...