big_sepM2_fmap and friends only work for nat keys
Iris version: dev.2019-11-22.2.a979391c
big_sepM2_fmap
, big_sepM2_fmap_l
and big_sepM2_fmap_r
only work for maps with nat
keys, but I don't see a fundamental reason for this. The problem is that they use (Φ : nat → A' → B' → PROP)
instead of (Φ : K → A' → B' → PROP)
. Let me know if I should open a PR which fixes this.