From 5ce1f2e2c54681241c87774f8773514d3e42ab7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 28 Mar 2022 19:48:34 +0200
Subject: [PATCH] Suppress use of image_eq.

---
 Lebesgue/Subset.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index d4a747ce..363785e5 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -2015,9 +2015,8 @@ Lemma image_of_preimage :
   forall A2, image f (preimage f A2) = inter A2 (image f fullset).
 Proof.
 intros A2; apply subset_ext; intros x2; split.
-intros [x1 Hx1]; easy.
-rewrite image_eq.
-intros [Hx2 [x1 [_ Hx1]]]; rewrite Hx1 in *; apply Im; easy.
+intros Hx2; induction Hx2 as [x1 Hx1]; easy.
+intros [Hx2 Hx2']; induction Hx2' as [x1 Hx1]; easy.
 Qed.
 
 Lemma image_of_preimage_of_image :
-- 
GitLab