From 6d2e61e15d82052b408054278e0b982e94f28de5 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. --- prelude/collections.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prelude/collections.v b/prelude/collections.v index 845c2e7b..9a08413f 100644 --- a/prelude/collections.v +++ b/prelude/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. -- 2.24.1