From 3103b7bf52d0275f2938d9af44ab2d0db89a6251 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 21:39:29 +0100
Subject: [PATCH] =?UTF-8?q?Lemma=20for=20X=20=E2=88=AA=20Y=20=E2=8A=86=20Z?=
 =?UTF-8?q?=20=E2=86=94=20X=20=E2=8A=86=20Z=20=E2=88=A7=20Y=20=E2=8A=86=20?=
 =?UTF-8?q?Z.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/collections.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index 4f43db43..5d560497 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -338,6 +338,8 @@ Section simple_collection.
   Proof. set_solver. Qed.
 
   (** Union *)
+  Lemma union_subseteq X Y Z : X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.
+  Proof. set_solver. Qed.
   Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
   Proof. set_solver. Qed.
   Lemma elem_of_union_l x X Y : x ∈ X → x ∈ X ∪ Y.
-- 
GitLab