diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2889ce04780b6bd2b4154c1af3e61914f97dc4d0..e9607aeffd30e960c7e03a85c268882b44da9356 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -579,7 +579,7 @@ Proof. apply insert_non_empty. Qed.
 Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = ∅.
 Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
 Lemma delete_singleton_ne {A} i j (x : A) :
-  j ≠ i → delete i {[j := x]} = {[j := x]}.
+  i ≠ j → delete i {[j := x]} = {[j := x]}.
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
 (** ** Properties of the map operations *)