From e7aa245af338965faf6624fbca179821f6c89b67 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 25 Mar 2022 16:36:01 +0100
Subject: [PATCH] Proof without image_eq.

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

diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index 6ed169ec..d4a747ce 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -144,6 +144,7 @@ Variable A1 : U1 -> Prop. (* Subset. *)
 Variable A2 : U2 -> Prop. (* Subset. *)
 
 Inductive image : U2 -> Prop := Im : forall x1, A1 x1 -> image (f x1).
+
 Definition image_ex : U2 -> Prop :=
   fun x2 => exists x1, A1 x1 /\ x2 = f x1.
 
@@ -1936,8 +1937,7 @@ Lemma preimage_empty_equiv :
   forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).
 Proof.
 intros A2; split.
-rewrite image_eq.
-intros HA2 x2 Hx2 [x1 [_ Hx1]]; apply (HA2 x1); rewrite Hx1 in Hx2; easy.
+intros HA2 x2 Hx2a Hx2b; induction Hx2b as [x1 Hx1]; apply (HA2 x1); easy.
 intros HA2 x1 Hx1; apply (HA2 (f x1)); easy.
 Qed.
 
-- 
GitLab