From 0a35ba520552a43fed233d5047e9945431229977 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Jan 2017 13:50:54 +0100
Subject: [PATCH] Fix more _L lemmas.

---
 theories/prelude/collections.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/prelude/collections.v b/theories/prelude/collections.v
index f85aeba06..3f6b96a3c 100644
--- a/theories/prelude/collections.v
+++ b/theories/prelude/collections.v
@@ -643,9 +643,9 @@ Section collection.
     Proof. unfold_leibniz; apply union_intersection_l. Qed.
     Lemma union_intersection_r_L X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z).
     Proof. unfold_leibniz; apply union_intersection_r. Qed.
-    Lemma intersection_union_l_L X Y Z : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z).
+    Lemma intersection_union_l_L X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z).
     Proof. unfold_leibniz; apply intersection_union_l. Qed.
-    Lemma intersection_union_r_L X Y Z : (X ∪ Y) ∩ Z ≡ (X ∩ Z) ∪ (Y ∩ Z).
+    Lemma intersection_union_r_L X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z).
     Proof. unfold_leibniz; apply intersection_union_r. Qed.
 
     (** Difference *)
-- 
GitLab