From 5631e485a821848a28824d43da37115c2aa0ee8a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 3 Oct 2016 09:28:17 +0200
Subject: [PATCH] Cancelation for union.

---
 prelude/collections.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/prelude/collections.v b/prelude/collections.v
index 39eb6f103..15920610a 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -339,6 +339,11 @@ Section simple_collection.
   Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
   Proof. set_solver. Qed.
 
+  Lemma union_cancel_l X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X ≡ Z ∪ Y → X ≡ Y.
+  Proof. set_solver. Qed.
+  Lemma union_cancel_r X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z ≡ Y ∪ Z → X ≡ Y.
+  Proof. set_solver. Qed.
+
   (** Empty *)
   Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
   Proof. set_solver. Qed.
@@ -455,6 +460,11 @@ Section simple_collection.
     Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
     Proof. unfold_leibniz. apply empty_union. Qed.
 
+    Lemma union_cancel_l_L X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X = Z ∪ Y → X = Y.
+    Proof. unfold_leibniz. apply union_cancel_l. Qed.
+    Lemma union_cancel_r_L X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z = Y ∪ Z → X = Y.
+    Proof. unfold_leibniz. apply union_cancel_r. Qed.
+
     (** Empty *)
     Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X.
     Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
-- 
GitLab