diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e04532a17525d7317e847e8d3887a7492ea2c51d..34bf85b682722b8bffc5f88c3eabb57e8aa00079 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2562,10 +2562,10 @@ Section kmap.
     rewrite lookup_kmap_is_Some. naive_solver.
   Qed.
   Lemma lookup_kmap {A} (m : M1 A) (i : K1) :
-    kmap f m !! f i = m !! i.
+    kmap f m !! (f i) = m !! i.
   Proof. apply option_eq. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
   Lemma lookup_total_kmap `{Inhabited A} (m : M1 A) (i : K1) :
-    kmap f m !!! f i = m !!! i.
+    kmap f m !!! (f i) = m !!! i.
   Proof. by rewrite !lookup_total_alt, lookup_kmap. Qed.
 
   Global Instance kmap_inj {A} : Inj (=@{M1 A}) (=) (kmap f).