Use `dom` instead of `∀ k, is_Some (.. !! k) ...`
See for example
The version with
dom is more intuitive, and likely easier to prove because one can reason equationally with lemmas for
dom. However, the fact that the set (here
gset) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.