From 7921671c2146147c79f6b34f187ebd342277f3e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Jul 2021 20:34:55 +0200
Subject: [PATCH] Add `singleton_subseteq_l` and `singleton_subseteq`.

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

diff --git a/theories/sets.v b/theories/sets.v
index 3bfef576..6ac9a22e 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -471,6 +471,11 @@ Section semi_set.
   Lemma not_elem_of_singleton_2 x y : x ≠ y → x ∉ ({[ y ]} : C).
   Proof. apply not_elem_of_singleton. Qed.
 
+  Lemma singleton_subseteq_l x X : {[ x ]} ⊆ X ↔ x ∈ X.
+  Proof. set_solver. Qed.
+  Lemma singleton_subseteq x y : {[ x ]} ⊆@{C} {[ y ]} ↔ x = y.
+  Proof. set_solver. Qed.
+
   (** Disjointness *)
   Lemma elem_of_disjoint X Y : X ## Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
   Proof. done. Qed.
-- 
GitLab