From 71e54c62fa89c23d3a694cbbf0528789c83ce487 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 23 Mar 2022 13:49:24 +0100
Subject: [PATCH] Try this one?

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

diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index 23b22001..b7fe5791 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -140,6 +140,11 @@ Variable f : U1 -> U2. (* Function. *)
 Variable A1 : U1 -> Prop. (* Subset. *)
 Variable A2 : U2 -> Prop. (* Subset. *)
 
+(* TODO: try with the following inductive type.
+Inductive image_alt : U2 -> Prop :=
+  | Im : forall x1, A1 x1 -> image_alt (f x1).
+*)
+
 Definition image : U2 -> Prop :=
   fun x2 => exists x1, A1 x1 /\ x2 = f x1.
 
-- 
GitLab