diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 33533c8cd11965eebe31b842af4deef5ffe1285b..29738bea0929be6d0f11c95ca2fe5f26a3b634b5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3355,6 +3355,14 @@ Section preimage.
       + apply set_choose_L in HXne as [j ?].
         apply (lookup_preimage_None_1 _ _ j) in HX'. naive_solver.
   Qed.
+
+  Lemma lookup_total_preimage m x i :
+    i ∈ map_preimage m !!! x ↔ m !! i = Some x.
+  Proof.
+    rewrite lookup_total_alt. destruct (map_preimage m !! x) as [X|] eqn:HX.
+    - by apply lookup_preimage_Some.
+    - rewrite lookup_preimage_None in HX. set_solver.
+  Qed.
 End preimage.
 
 (** * Tactics *)