Use type subset_system.

V -> A.

Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v

@@ -113,16 +113,16 @@ End Base_Def.
 Section Trace_Def.
 
 Context {U : Type}. (* Universe. *)
-Variable V : set U.
+Variable A : set U.
 Variable P : set_system U.
-Variable PV : set (subset V).
+Variable PA : subset_system A.
 
-Inductive Subset : set_system U := Sub : forall A, P A -> incl A V -> Subset A.
+Inductive Subset : set_system U := Sub : forall B, P B -> incl B A -> Subset B.
 
-Definition Lift : set_system U := fun A => PV (trace V A).
+Definition Lift : set_system U := fun B => PA (trace A B).
 
 (* Definition 226 p. 40 (v3) *)
-Inductive Trace : set (subset V) := Tr : forall A, P A -> Trace (trace V A).
+Inductive Trace : subset_system A := Tr : forall B, P B -> Trace (trace A B).
 
 End Trace_Def.