diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a109d8580ba00789812d43ff54d621aae9e36fe2..7bb6d2fe7bb879dd4fcff3931fc010087e498547 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -166,6 +166,8 @@ Context `{FinMap K M}.
 Section setoid.
   Context `{Equiv A}.
 
+  Lemma map_equiv_iff (m1 m2 : M A) : m1 ≡ m2 ↔ ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. done. Qed.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
     split; [intros Hm; apply map_eq; intros i|intros ->].