From dc7a3a899b9360f610f7e2bbcddd347e11abe5e1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Sep 2017 19:24:56 +0200
Subject: [PATCH] Put the inequality of delete_singleton_ne in the same
 direction as other _ne lemmas.

---
 theories/fin_maps.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2889ce04..e9607aef 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 *)
-- 
GitLab