diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d0f5cffddae4dd32f4af0c050abf69f2a0c7d69f..115ba5c5051fb6b73fa2e8563dc87bb77df85a76 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1395,6 +1395,10 @@ Section option.
       by eapply (cmra_validN_le n); last lia.
     - done.
   Qed.
+
+  Global Instance option_cancelable (ma : option A) :
+    (∀ a : A, IdFree a) → (∀ a : A, Cancelable a) → Cancelable ma.
+  Proof. destruct ma; apply _. Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 5df537032033b4a7e15be630cdc65ead3b1decc9..59230337296832a37a64068723e2ca9d3970672e 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -288,6 +288,12 @@ Proof.
   - by rewrite lookup_singleton_ne // !(left_id None _).
 Qed.
 
+Global Instance gmap_cancelable (m : gmap K A) :
+  (∀ x : A, IdFree x) → (∀ x : A, Cancelable x) → Cancelable m.
+Proof.
+  intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
+Qed.
+
 Lemma insert_op m1 m2 i x y :
   <[i:=x â‹… y]>(m1 â‹… m2) =  <[i:=x]>m1 â‹… <[i:=y]>m2.
 Proof. by rewrite (insert_merge (â‹…) m1 m2 i (x â‹… y) x y). Qed.