diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index 23b220013c3707005fd624b4e96bc77f0176ff11..b7fe5791222beddef16d55db19547c58d85a0587 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.