diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index bf91498c56cd817c4364e9b5d917b5c8e0709f57..a21b0eb163f37d36c1dd3f2d361e78542bc8dcd8 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -233,15 +233,15 @@ Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
     σ !! l2 = None →
     lit_eq σ (LitLoc l1) (LitLoc l2).
 
-Inductive lit_neq (σ : state) : base_lit → base_lit → Prop :=
+Inductive lit_neq : base_lit → base_lit → Prop :=
 | IntNeq z1 z2 :
-    z1 ≠ z2 → lit_neq σ (LitInt z1) (LitInt z2)
+    z1 ≠ z2 → lit_neq (LitInt z1) (LitInt z2)
 | LocNeq l1 l2 :
-    l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2)
+    l1 ≠ l2 → lit_neq (LitLoc l1) (LitLoc l2)
 | LocNeqNullR l :
-    lit_neq σ (LitLoc l) (LitInt 0)
+    lit_neq (LitLoc l) (LitInt 0)
 | LocNeqNullL l :
-    lit_neq σ (LitInt 0) (LitLoc l).
+    lit_neq (LitInt 0) (LitLoc l).
 
 Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_lit → Prop :=
 | BinOpPlus z1 z2 :
@@ -253,7 +253,7 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
 | BinOpEqTrue l1 l2 :
     lit_eq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool true)
 | BinOpEqFalse l1 l2 :
-    lit_neq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
+    lit_neq l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
 | BinOpOffset l z :
     bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ l +ₗ z).
 
@@ -302,7 +302,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
 | CasFailS l n e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
     σ !! l = Some (RSt n, LitV litl) →
-    lit_neq σ lit1 litl →
+    lit_neq lit1 litl →
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ lit_of_bool false) σ  []
 | CasSucS l e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
@@ -538,16 +538,11 @@ Lemma lit_eq_state σ1 σ2 l1 l2 :
   lit_eq σ1 l1 l2 → lit_eq σ2 l1 l2.
 Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
 
-Lemma lit_neq_state σ1 σ2 l1 l2 :
-  (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
-  lit_neq σ1 l1 l2 → lit_neq σ2 l1 l2.
-Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
-
 Lemma bin_op_eval_state σ1 σ2 op l1 l2 l' :
   (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
   bin_op_eval σ1 op l1 l2 l' → bin_op_eval σ2 op l1 l2 l'.
 Proof.
-  intros Heq. inversion 1; econstructor; eauto using lit_eq_state, lit_neq_state.
+  intros Heq. inversion 1; econstructor; eauto using lit_eq_state.
 Qed.
 
 (* Misc *)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 00bd52a0086378617623b45116f6c7ff67c905bd..26a0cdb0c327290daab6f25e1c5b9f58535f3898 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -20,7 +20,7 @@ Global Opaque iris_invG.
 Ltac inv_lit :=
   repeat match goal with
   | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
-  | H : lit_neq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
+  | H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_eq/=
   end.
 
 Ltac inv_bin_op_eval :=
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 834b8db7018e83cca45ba64cb93d9b0f4059f89a..befd4f4915836ce759f9c0f9b0fe0709f05d6d91 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -16,7 +16,7 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
     next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
 | Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
     IntoVal e1 (LitV lit1) → IntoVal e2 (LitV lit2) →
-    lit_neq σ lit1 litl → σ !! l = Some (st, LitV litl) →
+    lit_neq lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
 | Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
     IntoVal e1 (LitV lit1) → IntoVal e2 (LitV lit2) →
@@ -118,15 +118,9 @@ Proof.
   intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
   (* Oh my. FIXME. *)
-  - eapply lit_neq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
   - eapply lit_eq_state; last done.
     setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
     cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
-  - eapply lit_neq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
   - eapply lit_eq_state; last done.
     setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
     cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.