big_sepM2_fmap and friends only work for nat keys
Iris version: dev.2019-11-22.2.a979391c
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.