diff --git a/algebra/gmap.v b/algebra/gmap.v
index 5d658ea52ae0b942a03999e7f5f9ef1c1c3a77dd..aa08442b128f11c741466bfaffd0f8ad8f4b7a5f 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -195,6 +195,10 @@ Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types x y : A.
 
+Global Instance lookup_cmra_homomorphism :
+  UCMRAHomomorphism (lookup i : gmap K A → option A).
+Proof. split. split. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
+
 Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.