From 67db2f248ac8250c6b2de6e4e25701f517ec265c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 7 Aug 2020 10:43:33 +0200
Subject: [PATCH] add directional versions of not_elem_of_singleton

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

diff --git a/theories/sets.v b/theories/sets.v
index 2a97d742..749bd349 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -449,6 +449,10 @@ Section semi_set.
   Proof. set_solver. Qed.
   Lemma not_elem_of_singleton x y : x ∉ ({[ y ]} : C) ↔ x ≠ y.
   Proof. by rewrite elem_of_singleton. Qed.
+  Lemma not_elem_of_singleton_1 x y : x ∉ ({[ y ]} : C) → x ≠ y.
+  Proof. apply not_elem_of_singleton. Qed.
+  Lemma not_elem_of_singleton_2 x y : x ≠ y → x ∉ ({[ y ]} : C).
+  Proof. apply not_elem_of_singleton. Qed.
 
   (** Disjointness *)
   Lemma elem_of_disjoint X Y : X ## Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
-- 
GitLab