From de192271570cd447be69c5b0c552f8112bbee1df Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Jul 2021 21:28:15 +0200
Subject: [PATCH] make singleton submseteq lemma consistent with Iris

---
 theories/list.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/list.v b/theories/list.v
index 568cfc86..d568974e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2603,7 +2603,7 @@ Proof.
   by apply submseteq_skip, (submseteq_app_inv_l _ _ [x]).
 Qed.
 
-Lemma submseteq_singleton l x :
+Lemma singleton_submseteq_l l x :
   [x] ⊆+ l ↔ x ∈ l.
 Proof.
   split.
@@ -2613,6 +2613,9 @@ Proof.
     eapply take_drop_middle in Hlook; rewrite <-Hlook.
     eapply submseteq_cons_middle, submseteq_nil_l.
 Qed.
+Lemma singleton_submseteq x y :
+  [x] ⊆+ [y] ↔ x = y.
+Proof. rewrite singleton_submseteq_l. apply elem_of_list_singleton. Qed.
 
 Section submseteq_dec.
   Context `{!EqDecision A}.
-- 
GitLab