Lemma for X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.

3103b7bf · Robbert Krebbers · b8ffa59a · 3103b7bf
Commit 3103b7bf authored Feb 15, 2017 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/collections.v theories/collections.v +2 -0

No files found.
--- 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.