Use new API (liftp_any).

Renaming: Lift' -> Lift_full.
Rm Trace' (clearly equivalent to the new Trace).

Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v

@@ -118,13 +118,11 @@ Variable A : set U.
 Inductive Subset : set_system U -> set_system U :=
   | Sub : forall (P : set_system U) B, P B -> incl B A -> Subset P B.
 
-Definition Lift : subset_system A -> set_system U := image (lift A).
-Definition Lift' : subset_system A -> set_system U := fun PA B => PA (trace A B).
+Definition Lift : subset_system A -> set_system U := liftp_any A.
+Definition Lift_full : subset_system A -> set_system U := fun PA B => PA (trace A B).
 
 (* Definition 226 p. 40 (v3) *)
-Definition Trace : set_system U -> subset_system A := image (trace A).
-Inductive Trace' : set_system U -> subset_system A :=
-  | Tr : forall (P : set_system U) B, P B -> Trace' P (trace A B).
+Definition Trace : set_system U -> subset_system A := tracep_any A.
 
 End Trace_Def.