From 91ea2bfadace07229c9739cfe79a7226ad38535e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 07:32:57 +0200
Subject: [PATCH] Fix inconsistent arguments of `subset_difference_elem_of`.

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

diff --git a/theories/sets.v b/theories/sets.v
index f4b50688..f37e6869 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -677,7 +677,7 @@ Section set.
   Proof. set_solver. Qed.
   Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
   Proof. set_solver. Qed.
-  Lemma subset_difference_elem_of {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
+  Lemma subset_difference_elem_of x X : x ∈ X → X ∖ {[ x ]} ⊂ X.
   Proof. set_solver. Qed.
   Lemma difference_difference X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
   Proof. set_solver. Qed.
-- 
GitLab