From e920e2941c835ca345ddbfbec59f072acaa88c66 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 12 Jul 2016 16:50:06 +0200
Subject: [PATCH] Turn unused disjoint_union_difference into something more
sensible.
---
theories/collections.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/collections.v b/theories/collections.v
index 27e6830..888be9b 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -418,7 +418,7 @@ Section collection.
Proof. set_solver. Qed.
Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
Proof. set_solver. Qed.
- Lemma disjoint_union_difference X Y : X ⊥ Y → (X ∪ Y) ∖ X ≡ Y.
+ Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X.
Proof. set_solver. Qed.
Section leibniz.
@@ -438,8 +438,8 @@ Section collection.
Lemma difference_intersection_distr_l_L X Y Z :
(X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
- Lemma disjoint_union_difference_L X Y : X ⊥ Y → (X ∪ Y) ∖ X = Y.
- Proof. unfold_leibniz. apply disjoint_union_difference. Qed.
+ Lemma difference_disjoint_L X Y : X ⊥ Y → X ∖ Y = X.
+ Proof. unfold_leibniz. apply difference_disjoint. Qed.
End leibniz.
Section dec.
--
GitLab