Undesired simplification behaviour of big_sepM2

Iris version: dev.2019-11-22.2.a979391c

simpl unfolds the definition of big_sepM2 which makes it basically unusable.

Example:

From iris.program_logic Require Import weakestpre.

Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
  ([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => uPred_and ⌜∀ k : nat, is_Some (xs !! k) ↔ is_Some (ys !! k)⌝
    ([∗ map] xy ∈ map_zip xs ys, ⌜xy.1 = xy.2⌝%I) *)

I am currently using the following workaround (big_sepM2 does not seem to have an Arguments command at the moment):

Arguments big_sepM2 {PROP K _ _ A B} _ !_ !_ /.

Example big_sepM2_simpl Σ (xs ys : gmap nat nat):
  ([∗ map] x;y ∈ xs;ys, ⌜x=y⌝ : iProp Σ)%I.
Proof. simpl. Abort.
(* => ([∗ map] x;y ∈ xs;ys, ⌜x = y⌝)%I *)