Renaming: inj/Inj -> lift/Lft.

Lebesgue/Set_theory/Set_def_base.v

@@ -37,11 +37,11 @@ Definition subset : Type := set {x : U | A x}.
 Definition subset_system : Type := set subset.
 Definition subset_system_class : Type := set subset_system.
 
-Inductive inj (B : subset) (x : U) : Prop :=
-  | Inj : forall (Hx : A x), B (exist A x Hx) -> inj B x.
+Inductive lift (B : subset) (x : U) : Prop :=
+  | Lft : forall (Hx : A x), B (exist A x Hx) -> lift B x.
 Definition trace : set U -> subset := fun B x => B (skolem x).
 
-(*Coercion inj : subset >-> set. (* Is this correct? *)*)
+(*Coercion lift : subset >-> set. (* Is this correct? *)*)
 (*Coercion trace : set >-> subset. (* Is this correct? *)*)
 
 End Base_Def0.