From 157ae750316b4f0f5f1986bc79cdc9166eb2188a Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sat, 1 Feb 2020 23:43:02 +0100
Subject: [PATCH] Add lemma `not_elem_of_iff`.

---
 theories/sets.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/sets.v b/theories/sets.v
index 9ccac38b..d0dde8aa 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -562,6 +562,10 @@ Section semi_set.
     Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
   End leibniz.
 
+  Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
+    (x ∈ X ↔ x ∈ Y) ↔ (x ∉ X ↔ x ∉ Y).
+  Proof. destruct (decide (x ∈ X)), (decide (x ∈ Y)); tauto. Qed.
+
   Section dec.
     Context `{!RelDecision (≡@{C})}.
     Lemma set_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
-- 
GitLab