diff --git a/theories/collections.v b/theories/collections.v
index 1ef62bb2071850f359138b0a63cfb5050e62b0a5..8354bafda1ed136549c5a8054a7dd86b50cb3561 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.