`iInv` with cancellable invariants and a cinv_own token
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
iInv N with selpat can be an arbitrary selection pattern and not just one identifier.