Use `dom` instead of `∀ k, is_Some (.. !! k) ...`
See for example big_sepM_sep_zip_with
, big_sepM_sep_zip
, big_sepM2_intuitionistically_forall
, big_sepM2_forall
.
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.