Go for an inductive type too...

Lebesgue/Set_theory/Set_def_base.v

@@ -37,7 +37,9 @@ Definition subset : Type := set {x : U | A x}.
 Definition subset_system : Type := set subset.
 Definition subset_system_class : Type := set subset_system.
 
-Definition inj : subset -> set U :=
+Inductive inj (B : subset) (x : U) : Prop :=
+  | Inj : forall (Hx : A x), B (exist _ _ Hx) -> inj B x.
+Definition inj' : subset -> set U :=
   fun B x => exists (Hx : A x), B (exist _ _ Hx).
 Definition trace : set U -> subset := fun B x => B (skolem x).
 
@@ -202,7 +204,7 @@ Ltac set_unfold :=
     partition, disj, samef, inclf, same, incl,
       full, nonempty_ex, empty, (* Predicates. *)
     swap, prod, sym_diff, diff, add, inter, union, compl,
-      trace, inj, skolem, (* Operators. *)
+      trace, inj', skolem, (* Operators. *)
     pair, singleton, prop_cst, fullset, emptyset. (* Constructors. *)
 
 Ltac set_auto :=