diff --git a/Lebesgue/Set_theory/Set_system/Set_system_any.v b/Lebesgue/Set_theory/Set_system/Set_system_any.v
index 5b9814ace466c1e56b38e08feac898ef79ee8785..c3dc2c9cab0b70d5fb7ef0270c5f43a86ba404e5 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_any.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_any.v
@@ -364,9 +364,9 @@ Section Trace_Facts.
 
 Context {U : Type}.
 Variable P : set_system U.
-Variable V : set U.
+Variable A : set U.
 
-Lemma Trace_Open : is_Open P -> is_Open (Trace V P).
+Lemma Trace_Open : is_Open P -> is_Open (Trace A P).
 Proof.
 rewrite 2!is_Open_equiv; intros [HP1 [HP2 [HP3 HP4]]]; repeat split.
 apply Trace_wEmpty; easy.
@@ -375,7 +375,7 @@ apply Trace_Inter; easy.
 apply Trace_Unionf_any; easy.
 Qed.
 
-Lemma Trace_Closed : is_Closed P -> is_Closed (Trace V P).
+Lemma Trace_Closed : is_Closed P -> is_Closed (Trace A P).
 Proof.
 rewrite 2!is_Closed_equiv; intros [HP1 [HP2 [HP3 HP4]]]; repeat split.
 apply Trace_wEmpty; easy.
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_any.v b/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
index 95834b344397c71c7a20b988b0df341f5b4d2caf..3c96ff4d3f2721aa9c192a0e8450f9e43c89acb6 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
@@ -213,37 +213,37 @@ End Any_Facts2.
 Section Any_Facts3.
 
 Context {U : Type}.
-Variable V : set U.
+Variable A : set U.
 Variable P : set_system U.
 
-Lemma Trace_Interf_any : Interf_any P -> Interf_any (Trace V P).
+Lemma Trace_Interf_any : Interf_any P -> Interf_any (Trace A P).
 Proof.
-intros HP Idx A HIdx HA1.
-assert (HA2 : forall i, exists B, P B /\ A i = trace V B).
-  intros i; induction (HA1 i) as [B HB]; exists B; easy.
-destruct (choice _ HA2) as [B HB].
-replace (interf_any A) with (interf_any (tracef_map_any V B)).
+intros HP Idx BA HIdx HBA1.
+assert (HBA2 : forall i, exists B, P B /\ BA i = trace A B).
+  intros i; induction (HBA1 i) as [B HB]; exists B; easy.
+destruct (choice _ HBA2) as [B HB].
+replace (interf_any BA) with (interf_any (tracef_map_any A B)).
 rewrite <- trace_interf_any; apply Im, HP, HB; easy.
 apply interf_any_ext; intros i; symmetry; apply HB.
 Qed.
 
-Lemma Trace_Unionf_any : Unionf_any P -> Unionf_any (Trace V P).
+Lemma Trace_Unionf_any : Unionf_any P -> Unionf_any (Trace A P).
 Proof.
-intros HP Idx A HIdx HA1.
-assert (HA2 : forall i, exists B, P B /\ A i = trace V B).
-  intros i; induction (HA1 i) as [B HB]; exists B; easy.
-destruct (choice _ HA2) as [B HB].
-replace (unionf_any A) with (unionf_any (tracef_map_any V B)).
+intros HP Idx BA HIdx HBA1.
+assert (HBA2 : forall i, exists B, P B /\ BA i = trace A B).
+  intros i; induction (HBA1 i) as [B HB]; exists B; easy.
+destruct (choice _ HBA2) as [B HB].
+replace (unionf_any BA) with (unionf_any (tracef_map_any A B)).
 rewrite <- trace_unionf_any; apply Im, HP, HB; easy.
 apply unionf_any_ext; intros i; symmetry; apply HB.
 Qed.
 
-Lemma Trace_Inter_any : Inter_any P -> Inter_any (Trace V P).
+Lemma Trace_Inter_any : Inter_any P -> Inter_any (Trace A P).
 Proof.
 rewrite <- 2!Interf_any_Inter_any_equiv; apply Trace_Interf_any.
 Qed.
 
-Lemma Trace_Union_any : Union_any P -> Union_any (Trace V P).
+Lemma Trace_Union_any : Union_any P -> Union_any (Trace A P).
 Proof.
 rewrite <- 2!Unionf_any_Union_any_equiv; apply Trace_Unionf_any.
 Qed.
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_base.v b/Lebesgue/Set_theory/Set_system/Set_system_base_base.v
index d49d9d16824598ee3fb3c3ae6a7625574a985375..b254ef1cdf5a422796b5c2c2127bb68df6786d4a 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_base.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_base.v
@@ -396,7 +396,8 @@ apply Lift_Lift_full.
 rewrite <- compose_eq, Trace_Lift; easy.
 Qed.
 
-Lemma Trace_equiv : forall (P : set_system U) B, Trace A P B <-> exists C, P C /\ B = trace A C.
+Lemma Trace_equiv :
+  forall (P : set_system U) B, Trace A P B <-> exists C, P C /\ B = trace A C.
 Proof.
 intros B; split.
 intros [C HC]; exists C; easy.
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v b/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v
index 19c5dd22ec6af5139bcdacbd1f7fee3ccd968edc..90f957758eb406eb59cf7fa1b228f43aa01ec81f 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_finite.v
@@ -343,15 +343,15 @@ End Finite_Facts2.
 Section Finite_Facts3.
 
 Context {U : Type}.
-Variable V : set U.
+Variable A : set U.
 Variable P : set_system U.
 
-Lemma Trace_Inter_finite : Inter_finite P -> Inter_finite (Trace V P).
+Lemma Trace_Inter_finite : Inter_finite P -> Inter_finite (Trace A P).
 Proof.
 rewrite 2!Inter_finite_equiv; apply Trace_Inter.
 Qed.
 
-Lemma Trace_Union_finite : Union_finite P -> Union_finite (Trace V P).
+Lemma Trace_Union_finite : Union_finite P -> Union_finite (Trace A P).
 Proof.
 rewrite 2!Union_finite_equiv; apply Trace_Union.
 Qed.
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v b/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v
index c9e466b41e1389a5b0020a429040c5e77c1ca9de..fff5dacf5de15101e93de56d0966732adcfbff4e 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_seq.v
@@ -352,36 +352,36 @@ End Seq_Facts2.
 Section Seq_Facts3.
 
 Context {U : Type}.
-Variable V : set U.
+Variable A : set U.
 Variable P : set_system U.
 
-Lemma Trace_Inter_seq : Inter_seq P -> Inter_seq (Trace V P).
+Lemma Trace_Inter_seq : Inter_seq P -> Inter_seq (Trace A P).
 Proof.
-intros HP A HA1.
-assert (HA2 : forall n, exists B, P B /\ A n = trace V B).
-  intros n; induction (HA1 n) as [B HB]; exists B; easy.
-destruct (choice _ HA2) as [B HB].
-replace (inter_seq A) with (inter_seq (tracem_seq V B)).
+intros HP BA HBA1.
+assert (HBA2 : forall n, exists B, P B /\ BA n = trace A B).
+  intros n; induction (HBA1 n) as [B HB]; exists B; easy.
+destruct (choice _ HBA2) as [B HB].
+replace (inter_seq BA) with (inter_seq (tracem_seq A B)).
 rewrite <- trace_inter_seq; apply Im, HP, HB.
 apply inter_seq_ext; intros n; symmetry; apply HB.
 Qed.
 
-Lemma Trace_Union_seq : Union_seq P -> Union_seq (Trace V P).
+Lemma Trace_Union_seq : Union_seq P -> Union_seq (Trace A P).
 Proof.
-intros HP A HA1.
-assert (HA2 : forall n, exists B, P B /\ A n = trace V B).
-  intros n; induction (HA1 n) as [B HB]; exists B; easy.
-destruct (choice _ HA2) as [B HB].
-replace (union_seq A) with (union_seq (tracem_seq V B)).
+intros HP BA HBA1.
+assert (HBA2 : forall n, exists B, P B /\ BA n = trace A B).
+  intros n; induction (HBA1 n) as [B HB]; exists B; easy.
+destruct (choice _ HBA2) as [B HB].
+replace (union_seq BA) with (union_seq (tracem_seq A B)).
 rewrite <- trace_union_seq; apply Im, HP, HB.
 apply union_seq_ext; intros n; symmetry; apply HB.
 Qed.
 
 (* These results are wrong!
 
-Lemma Trace_Inter_monot_seq : Inter_monot_seq P -> Inter_monot_seq (Trace V P).
-Lemma Trace_Union_monot_seq : Union_monot_seq P -> Union_monot_seq (Trace V P).
-Lemma Trace_Union_disj_seq : Union_disj_seq P -> Union_disj_seq (Trace V P).
+Lemma Trace_Inter_monot_seq : Inter_monot_seq P -> Inter_monot_seq (Trace A P).
+Lemma Trace_Union_monot_seq : Union_monot_seq P -> Union_monot_seq (Trace A P).
+Lemma Trace_Union_disj_seq : Union_disj_seq P -> Union_disj_seq (Trace A P).
 
 Indeed, monotonic or disjoint traces do not imply that the initial sequence is.
 Thus, we cannot use the hypothesis... *)
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_finite.v b/Lebesgue/Set_theory/Set_system/Set_system_finite.v
index 53c316ff4d64d33412e2626ace37c67cadf27bdf..b33dfc2fef2bb064c6592d4eb1e4f345587c8ae1 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_finite.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_finite.v
@@ -877,15 +877,15 @@ Section Trace_Facts.
 
 Context {U : Type}.
 Variable P : set_system U.
-Variable A0 V : set U.
+Variable A0 A : set U.
 
-Lemma Trace_Psyst : is_Psyst P A0 -> is_Psyst (Trace V P) (trace V A0).
+Lemma Trace_Psyst : is_Psyst P A0 -> is_Psyst (Trace A P) (trace A A0).
 Proof.
 rewrite 2!Psyst_equiv; intros [HP1 HP2]; split; try easy.
 apply Trace_Inter; easy.
 Qed.
 
-Lemma Trace_Ring : is_Ring P -> is_Ring (Trace V P).
+Lemma Trace_Ring : is_Ring P -> is_Ring (Trace A P).
 Proof.
 rewrite 2!Ring_equiv; intros [HP1 [HP2 HP3]]; repeat split.
 apply Trace_wEmpty; easy.
@@ -893,7 +893,7 @@ apply Trace_Diff; easy.
 apply Trace_Union; easy.
 Qed.
 
-Lemma Trace_Algebra : is_Algebra P -> is_Algebra (Trace V P).
+Lemma Trace_Algebra : is_Algebra P -> is_Algebra (Trace A P).
 Proof.
 rewrite 2!Algebra_equiv; intros [HP1 [HP2 HP3]]; repeat split.
 apply Trace_wEmpty; easy.
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_seq.v b/Lebesgue/Set_theory/Set_system/Set_system_seq.v
index 191d45300df6d462ecaa02fb52afd3a6a9240abe..451ff01d0cbc4168cf2f260b9346b3730e8ae909 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_seq.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_seq.v
@@ -1165,13 +1165,13 @@ Section Trace_Facts.
 
 Context {U : Type}.
 Variable P : set_system U.
-Variable V : set U.
+Variable A : set U.
 
 (* These results are wrong since unitary results are!
-Lemma Trace_Monotone_class : is_Monotone_class P -> is_Monotone_class (Trace V P).
-Lemma Trace_Lsyst : is_Lsyst P -> is_Lsyst (Trace V P). *)
+Lemma Trace_Monotone_class : is_Monotone_class P -> is_Monotone_class (Trace A P).
+Lemma Trace_Lsyst : is_Lsyst P -> is_Lsyst (Trace A P). *)
 
-Lemma Trace_Sigma_ring : is_Sigma_ring P -> is_Sigma_ring (Trace V P).
+Lemma Trace_Sigma_ring : is_Sigma_ring P -> is_Sigma_ring (Trace A P).
 Proof.
 rewrite 2!Sigma_ring_equiv; intros [HP1 [HP2 HP3]]; repeat split.
 apply Trace_wEmpty; easy.
@@ -1179,7 +1179,7 @@ apply Trace_Diff; easy.
 apply Trace_Union_seq; easy.
 Qed.
 
-Lemma Trace_Sigma_algebra : is_Sigma_algebra P -> is_Sigma_algebra (Trace V P).
+Lemma Trace_Sigma_algebra : is_Sigma_algebra P -> is_Sigma_algebra (Trace A P).
 Proof.
 rewrite 2!Sigma_algebra_equiv; intros [HP1 [HP2 HP3]]; repeat split.
 apply Trace_wEmpty; easy.
@@ -1193,7 +1193,7 @@ End Trace_Facts.
 Section Sigma_algebra_Prod_Facts1.
 
 Context {U1 U2 : Type}.
-Variable genU1 : set_system U1.
+Aariable genU1 : set_system U1.
 Variable genU2 : set_system U2.
 
 Let genU1xU2 := Gen_Prod genU1 genU2.