diff --git a/theories/lang/races.v b/theories/lang/races.v
index c247955ce23d2656c8f170a7a6c6bcf04c2577e1..0c0f6ca7c428d6391504e91bf1006cb06e2a42ff 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -119,15 +119,15 @@ Proof.
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
   (* Oh my. FIXME. *)
   - eapply lit_eq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
     rename select loc into l.
     rename select state into σ.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
   - eapply lit_eq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
     rename select loc into l.
     rename select state into σ.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
 Qed.
 
 Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :