`iInv`: support tokens that are "framed" around the accessor
I have cancellable invariant and cinv_own
token in a proposition "Hp", then usually I don't want to touch "Hp" when opening an invariant. However, if I use iInv
I have to explicitly name "Hp" again:
iInv N with "Hp" as "[H Hp]" "Hcl"
This also prevents me from using the (x1 x2) "..."
introduction pattern. E.g. instead of
iInv N with "Hp" as (x) "[H1 H2]" "Hcl"
one has to write
iInv N with "Hp" as "[H Hp]" "Hcl";
iDestruct "H" as (x) "[H1 H2]"
It is not immediately obvious how to modify the tactics, because in general the selpat
in iInv N with selpat
can be an arbitrary selection pattern and not just one identifier.