diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6dd3439030f094624e4174c86d85b2e958a84927..54670738d570f38ba1cec56fc93ec6f4d7d1e900 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,8 @@ lemma.
 
 * Add a construction `bi_tc` to create transitive closures of
   PROP-level binary relations.
+* Use `binder` in notations for big ops. This means one can write things such
+  as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/notation.v b/iris/bi/notation.v
index 4ca6fddcbb277d624b89931a794c556a79d69e04..d7f4110270a4ebc3e98097fe875d7ae64b0ea335 100644
--- a/iris/bi/notation.v
+++ b/iris/bi/notation.v
@@ -124,66 +124,68 @@ Reserved Notation "P ={ E }▷=∗^ n Q"
 
 (** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
-  (at level 200, l at level 10, k, x at level 1, right associativity,
+  (at level 200, l at level 10, k binder, x binder, right associativity,
    format "[∗  list]  k ↦ x  ∈  l ,  P").
 Reserved Notation "'[∗' 'list]' x ∈ l , P"
-  (at level 200, l at level 10, x at level 1, right associativity,
+  (at level 200, l at level 10, x binder, right associativity,
    format "[∗  list]  x  ∈  l ,  P").
 
 Reserved Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P"
-  (at level 200, l1, l2 at level 10, k, x1, x2 at level 1, right associativity,
+  (at level 200, l1, l2 at level 10, k binder, x1 binder, x2 binder,
+   right associativity,
    format "[∗  list]  k ↦ x1 ; x2  ∈  l1 ; l2 ,  P").
 Reserved Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P"
-  (at level 200, l1, l2 at level 10, x1, x2 at level 1, right associativity,
+  (at level 200, l1, l2 at level 10, x1 binder, x2 binder, right associativity,
    format "[∗  list]  x1 ; x2  ∈  l1 ; l2 ,  P").
 
 Reserved Notation "'[∗]' Ps" (at level 20).
 
 Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P"
-  (at level 200, l at level 10, k, x at level 1, right associativity,
+  (at level 200, l at level 10, k binder, x binder, right associativity,
    format "[∧  list]  k ↦ x  ∈  l ,  P").
 Reserved Notation "'[∧' 'list]' x ∈ l , P"
-  (at level 200, l at level 10, x at level 1, right associativity,
+  (at level 200, l at level 10, x binder, right associativity,
    format "[∧  list]  x  ∈  l ,  P").
 
 Reserved Notation "'[∧]' Ps" (at level 20).
 
 Reserved Notation "'[∨' 'list]' k ↦ x ∈ l , P"
-  (at level 200, l at level 10, k, x at level 1, right associativity,
+  (at level 200, l at level 10, k binder, x binder, right associativity,
    format "[∨  list]  k ↦ x  ∈  l ,  P").
 Reserved Notation "'[∨' 'list]' x ∈ l , P"
-  (at level 200, l at level 10, x at level 1, right associativity,
+  (at level 200, l at level 10, x binder, right associativity,
    format "[∨  list]  x  ∈  l ,  P").
 
 Reserved Notation "'[∨]' Ps" (at level 20).
 
 Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
-  (at level 200, m at level 10, k, x at level 1, right associativity,
+  (at level 200, m at level 10, k binder, x binder, right associativity,
    format "[∗  map]  k ↦ x  ∈  m ,  P").
 Reserved Notation "'[∗' 'map]' x ∈ m , P"
-  (at level 200, m at level 10, x at level 1, right associativity,
+  (at level 200, m at level 10, x binder, right associativity,
    format "[∗  map]  x  ∈  m ,  P").
 
 Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
-  (at level 200, m1, m2 at level 10, k, x1, x2 at level 1, right associativity,
+  (at level 200, m1, m2 at level 10,
+   k binder, x1 binder, x2 binder, right associativity,
    format "[∗  map]  k ↦ x1 ; x2  ∈  m1 ; m2 ,  P").
 Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
-  (at level 200, m1, m2 at level 10, x1, x2 at level 1, right associativity,
+  (at level 200, m1, m2 at level 10, x1 binder, x2 binder, right associativity,
    format "[∗  map]  x1 ; x2  ∈  m1 ; m2 ,  P").
 
 Reserved Notation "'[∧' 'map]' k ↦ x ∈ m , P"
-  (at level 200, m at level 10, k, x at level 1, right associativity,
+  (at level 200, m at level 10, k binder, x binder, right associativity,
    format "[∧  map]  k ↦ x  ∈  m ,  P").
 Reserved Notation "'[∧' 'map]' x ∈ m , P"
-  (at level 200, m at level 10, x at level 1, right associativity,
+  (at level 200, m at level 10, x binder, right associativity,
    format "[∧  map]  x  ∈  m ,  P").
 
 Reserved Notation "'[∗' 'set]' x ∈ X , P"
-  (at level 200, X at level 10, x at level 1, right associativity,
+  (at level 200, X at level 10, x binder, right associativity,
    format "[∗  set]  x  ∈  X ,  P").
 
 Reserved Notation "'[∗' 'mset]' x ∈ X , P"
-  (at level 200, X at level 10, x at level 1, right associativity,
+  (at level 200, X at level 10, x binder, right associativity,
    format "[∗  mset]  x  ∈  X ,  P").
 
 (** Define the scope *)
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ae781fa791f05fce6e64f6b6ead3dd7191d73dbe..72f78ee78b9a08733e93e00cb05ed222e2df231e 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -230,7 +230,10 @@ Proof.
   rewrite replicate_length in Hlen2; subst.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
   rewrite -plus_n_O.
-  iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'"); [congruence| |]; last first.
+  iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'");
+    (* FIXME: Different implicit types for [length] are inferred, so [lia] and
+    [congruence] do not work due to https://github.com/coq/coq/issues/16634 *)
+    [by rewrite Hlen1 Hlen3| |]; last first.
   { by rewrite big_sepL2_replicate_r // big_sepL_omap. }
   (* we run the adequacy proof again to get this assumption *)
   iPureIntro. intros e2 -> Hel.
diff --git a/tests/bi.ref b/tests/bi.ref
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..3501bc76ecfd2a8f1b503ae9b870dda364b97a14 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -0,0 +1,6 @@
+The command has indeed failed with message:
+In environment
+PROP : bi
+m : gmap nat nat
+The term "m" has type "gmap nat nat" while it is expected to have type
+ "gmap nat Z" (cannot unify "nat" and "Z").
diff --git a/tests/bi.v b/tests/bi.v
index 87f512560dbe489651c9020674a0d93f7c52ced6..299a8bd3da335b979195624b4babcb3919896555 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -1,4 +1,6 @@
-From iris.bi Require Import bi plainly.
+From iris.bi Require Import bi plainly big_op.
+
+Unset Mangle Names.
 
 (** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
 Lemma test_impl_persistent_1 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
@@ -14,3 +16,47 @@ Proof.
   (* [<affine> True] is implicitly in %I scope. *)
   pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
 Abort.
+
+(** Some basic tests to make sure patterns work in big ops. *)
+Definition big_sepM_pattern_value
+    {PROP : bi} (m : gmap nat (nat * nat)) : PROP :=
+  [∗ map] '(x,y) ∈ m, ⌜ 10 = x ⌝.
+
+Definition big_sepM_pattern_value_tt
+    {PROP : bi} (m : gmap nat ()) : PROP :=
+  [∗ map] '() ∈ m, True.
+
+Inductive foo := Foo (n : nat).
+
+Definition big_sepM_pattern_value_custom
+    {PROP : bi} (m : gmap nat foo) : PROP :=
+  [∗ map] '(Foo x) ∈ m, ⌜ 10 = x ⌝.
+
+Definition big_sepM_pattern_key
+    {PROP : bi} (m : gmap (nat * nat) nat) : PROP :=
+  [∗ map] '(k,_) ↦ _ ∈ m, ⌜ 10 = k ⌝.
+
+Definition big_sepM_pattern_both
+    {PROP : bi} (m : gmap (nat * nat) (nat * nat)) : PROP :=
+  [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.
+
+Definition big_sepM2_pattern {PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP :=
+  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
+
+(** This fails, Coq will infer [x] to have type [Z] due to the equality, and
+then sees a type mismatch with [m : gmap nat nat]. *)
+Fail Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP :=
+  [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.
+
+(** With a cast, we can force Coq to type check the body with [x : nat] and
+thereby insert the [nat] to [Z] coercion in the body. *)
+Definition big_sepM_cast {PROP : bi} (m : gmap nat nat) : PROP :=
+  [∗ map] (x:nat) ∈ m, ⌜ 10%Z = x ⌝.
+
+Section big_sepM_implicit_type.
+  Implicit Types x : nat.
+
+  (** And we can do the same with an [Implicit Type]. *)
+  Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP :=
+    [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.
+End big_sepM_implicit_type.