diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 84f36d956b9c84c6cb640650226fad1a5debdac9..cff6fd424914db4b49202165b3d74af22ccb70eb 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -90,10 +90,7 @@ Proof.
   destruct (decide (i = j)); set_solver.
 Qed.
 Lemma dom_insert_lookup {A} (m : M A) i x :
-  is_Some (m !! i) → dom D (<[i:=x]>m) ≡ dom D m.
-Proof.
-  intros Hindom%elem_of_dom. rewrite dom_insert. set_solver.
-Qed.
+Proof. intros Hindom%elem_of_dom. rewrite dom_insert. set_solver. Qed.
 Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
 Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :