From dc3b0de33ad3a460b9cdcb7e48317b2fa186a9f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 16 Mar 2022 20:13:55 +0100
Subject: [PATCH] Equiv -> impl.

---
 Lebesgue/Subset_Rbar.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lebesgue/Subset_Rbar.v b/Lebesgue/Subset_Rbar.v
index 590173b4..1b3a7899 100644
--- a/Lebesgue/Subset_Rbar.v
+++ b/Lebesgue/Subset_Rbar.v
@@ -913,7 +913,7 @@ Proof.
 apply Ext_equiv; split; intros B HB.
 (* *)
 induction HB as [A HA | B HB].
-apply R_Rbar_open_equiv; easy.
+apply open_R_Rbar; easy.
 induction HB as [A B1 HA HB1 | A a b HA]; repeat apply open_or.
 1,3: apply R_Rbar_open_equiv; easy.
 1,2,3: apply Rbar_ray_open_is_open; try easy.
-- 
GitLab