diff --git a/coq/ra/base/ghosts.v b/coq/ra/base/ghosts.v
index aed4269c4ee9713fe78332b9641a795b3107c9ba..ca0d073db122185a8d55fec528b1d74b14fd888d 100644
--- a/coq/ra/base/ghosts.v
+++ b/coq/ra/base/ghosts.v
@@ -366,7 +366,7 @@ Section Exclusives.
   Lemma gmapR_singleton_Exclusive (i: K) (x y: A) `{!Exclusive x}:
     ✓ ({[i := x]} ⋅ {[i := y]}) → False.
   Proof.
-    intros ?. rewrite op_singleton. move/(_ i). rewrite lookup_singleton.
+    rewrite op_singleton. move/(_ i). rewrite lookup_singleton.
     by apply exclusive_l.
   Qed.