From fd8a6717a2610c00dec920ee5f33b00b14ef1fbf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Mar 2017 21:49:58 +0100
Subject: [PATCH] Prove empty_subseteq.

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

diff --git a/theories/collections.v b/theories/collections.v
index 1ef62bb2..8354bafd 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -373,6 +373,8 @@ Section simple_collection.
   Proof. set_solver. Qed.
 
   (** Empty *)
+  Lemma empty_subseteq X : ∅ ⊆ X.
+  Proof. set_solver. Qed.
   Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
   Proof. set_solver. Qed.
   Lemma elem_of_empty x : x ∈ ∅ ↔ False.
-- 
GitLab