iInv does not behave as intended when the goal is an accessor
When the goal is of the form
|={⊤,∅}=> ∃ ..., P ∗ (Q ={∅,⊤}=∗ Φ )
I would hope iInv N
where the invariant assertion is I
to turn it into something like
|={N,∅}=> ∃ ..., P ∗ (I * Q ={∅,⊤}=∗ Φ )
but currently we have no good way to even detect the goal as an accessor, so none of this can happen.