diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index fd4df4077a947e71a69c410b39c14357bbda90cc..54b81d30e5f50889455a07253819e54e677fbd3f 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -2,6 +2,7 @@ From iris.algebra Require Export cmra.
 From stdpp Require Export gmap.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 Section cofe.
@@ -236,6 +237,9 @@ Qed.
 Lemma op_singleton (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
+Global Instance is_op_singleton i a a1 a2 :
+  IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
+Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -op_singleton. Qed.
 
 Global Instance gmap_core_id m : (∀ x : A, CoreId x) → CoreId m.
 Proof.