diff --git a/Lebesgue/Subset_seq.v b/Lebesgue/Subset_seq.v
index 04132f8ed513d7eaf0f0fd1781f6d1f371525211..091527bb1ab8a90317f1ae31ee74b49a30906235 100644
--- a/Lebesgue/Subset_seq.v
+++ b/Lebesgue/Subset_seq.v
@@ -56,7 +56,7 @@ Definition incl_seq : Prop :=
   forall n, incl (A n) (B n).
 
 Definition same_seq : Prop :=
-  forall n, same (A n) (B n).
+  forall n, same (A n) (B n). (* Should be A n = B n ? *)
 
 (* Warning: incr actually means nondecreasing. *)
 Definition incr_seq : Prop :=
diff --git a/Lebesgue/measurable-new.v b/Lebesgue/measurable-new.v
deleted file mode 100644
index b1ce5984e83b6b8d9a21e6a09839d3fe41fb85ad..0000000000000000000000000000000000000000
--- a/Lebesgue/measurable-new.v
+++ /dev/null
@@ -1,596 +0,0 @@
-(**
-This file is part of the Elfic library
-
-Copyright (C) Boldo, Clément, Faissole, Martin, Mayero, Mouhcine
-
-This library is free software; you can redistribute it and/or
-modify it under the terms of the GNU Lesser General Public
-License as published by the Free Software Foundation; either
-version 3 of the License, or (at your option) any later version.
-
-This library is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-COPYING file for more details.
-*)
-
-(** Definition and properties of the concept of measurability
- for subsets of a given type.
-
- This is merely an interface for the definition and main properties
- of sigma-algebras from the file Subset_system.v where "measurable" is used
- instead of "Sigma_algebra" in almost all lemma names and statements. *)
-
-From Coq Require Import ClassicalChoice.
-From Coq Require Import Lia.
-From Coquelicot Require Import Hierarchy.
-
-Require Import UniformSpace_compl.
-Require Import Subset Subset_finite Subset_seq.
-Require Import Subset_system_base Subset_system_gen Subset_system.
-
-Open Scope nat_scope.
-
-
-Section measurable_Facts.
-
-(** Definition and properties of the measurability of subset. *)
-
-Context {E : Type}. (* Universe. *)
-Variable genE : (E -> Prop) -> Prop. (* Generator. *)
-
-Definition measurable : (E -> Prop) -> Prop := Sigma_algebra genE.
-
-Definition measurable_finite : (nat -> E -> Prop) -> nat -> Prop :=
-  fun A N => forall n, n < S N -> measurable (A n).
-
-Definition measurable_seq : (nat -> E -> Prop) -> Prop :=
-  fun A => forall n, measurable (A n).
-
-Lemma measurable_ext :
-  forall A1 A2, same A1 A2 -> measurable A1 -> measurable A2.
-Proof.
-intros A1 A2 H H1; apply subset_ext in H; now rewrite <- H.
-Qed.
-
-Lemma measurable_finite_ext :
-  forall A1 A2 N,
-    same_finite A1 A2 N -> measurable_finite A1 N -> measurable_finite A2 N.
-Proof.
-intros A1 A2 N H H1 n Hn; apply subset_finite_ext with (2 := Hn) in H.
-rewrite <- H; now apply (H1 n).
-Qed.
-
-Lemma measurable_seq_ext :
-  forall A1 A2, same_seq A1 A2 -> measurable_seq A1 -> measurable_seq A2.
-Proof.
-intros A1 A2 H H1; apply subset_seq_ext in H; now rewrite <- H.
-Qed.
-
-Lemma measurable_empty : measurable emptyset. (* wEmpty measurable. *)
-Proof.
-apply Sigma_algebra_wEmpty.
-Qed.
-
-Lemma measurable_full : measurable fullset. (* wFull measurable. *)
-Proof.
-apply Sigma_algebra_wFull.
-Qed.
-
-Lemma measurable_Prop : forall P, measurable (Prop_cst P).
-Proof.
-apply Sigma_algebra_Prop.
-Qed.
-
-Lemma measurable_compl :
-  forall A, measurable A -> measurable (compl A).
-  (* Compl measurable. *)
-Proof.
-apply Sigma_algebra_Compl.
-Qed.
-
-Lemma measurable_compl_rev :
-  forall A, measurable (compl A) -> measurable A.
-  (* Compl_rev measurable. *)
-Proof.
-apply Sigma_algebra_Compl_rev.
-Qed.
-
-Lemma measurable_union :
-  forall A1 A2, measurable A1 -> measurable A2 -> measurable (union A1 A2).
-  (* Union measurable. *)
-Proof.
-apply Sigma_algebra_Union.
-Qed.
-
-Lemma measurable_inter :
-  forall A1 A2, measurable A1 -> measurable A2 -> measurable (inter A1 A2).
-  (* Inter measurable. *)
-Proof.
-apply Sigma_algebra_Inter.
-Qed.
-
-Lemma measurable_union_finite :
-  forall A N, measurable_finite A N -> measurable (union_finite A N).
-  (* Union_finite measurable. *)
-Proof.
-apply Sigma_algebra_Union_finite.
-Qed.
-
-Lemma measurable_inter_finite :
-  forall A N, measurable_finite A N -> measurable (inter_finite A N).
-  (* Inter_finite measurable. *)
-Proof.
-apply Sigma_algebra_Inter_finite.
-Qed.
-
-Lemma measurable_union_seq :
-  forall A, measurable_seq A -> measurable (union_seq A).
-  (* Union_seq measurable. *)
-Proof.
-apply Sigma_algebra_Union_seq.
-Qed.
-
-Lemma measurable_inter_seq :
-  forall A, measurable_seq A -> measurable (inter_seq A).
-  (* Inter_seq measurable. *)
-Proof.
-apply Sigma_algebra_Inter_seq.
-Qed.
-
-Lemma measurable_diff :
-  forall A1 A2, measurable A1 -> measurable A2 -> measurable (diff A1 A2).
-  (* Diff measurable. *)
-Proof.
-apply Sigma_algebra_Diff.
-Qed.
-
-Lemma measurable_FU :
-  forall A N, measurable_finite A N -> measurable_finite (FU A) N.
-Proof.
-intros A N HA n Hn; apply measurable_union_finite.
-intros m Hm; apply HA; lia.
-Qed.
-
-(* From Lemma 480 pp. 84-85 (v2) *)
-Lemma measurable_DU :
-  forall A, measurable_seq A -> measurable_seq (DU A).
-Proof.
-intros A HA n; destruct n; simpl; try easy.
-apply measurable_diff; try easy.
-now apply measurable_union_finite.
-Qed.
-
-End measurable_Facts.
-
-
-Section measurable_gen_Facts1.
-
-Context {E : Type}. (* Universe. *)
-
-(** Correcness result. *)
-
-Lemma measurable_correct :
-  forall P : ((E -> Prop) -> Prop) -> Prop,
-    IIncl is_Sigma_algebra P <-> forall gen, P (measurable gen).
-Proof.
-apply Sigma_algebra_correct.
-Qed.
-
-(** Properties of the "generation" of measurability. *)
-
-Variable genE : (E -> Prop) -> Prop. (* Generator. *)
-
-Lemma measurable_gen : Incl genE (measurable genE).
-Proof.
-apply Sigma_algebra_Gen.
-Qed.
-
-Lemma measurable_gen_idem : is_Sigma_algebra (measurable genE).
-Proof.
-apply Sigma_algebra_idem.
-Qed.
-
-Lemma measurable_gen_monot :
-  forall genE', Incl genE genE' -> Incl (measurable genE) (measurable genE').
-Proof.
-apply Sigma_algebra_monot.
-Qed.
-
-Lemma measurable_gen_lub_alt :
-  forall P, is_Sigma_algebra P -> Incl genE P -> Incl (measurable genE) P.
-Proof.
-intros P; apply Sigma_algebra_lub.
-Qed.
-
-Lemma measurable_gen_lub :
-  forall genE',
-    Incl genE (measurable genE') -> Incl (measurable genE) (measurable genE').
-Proof.
-apply Sigma_algebra_lub_alt.
-Qed.
-
-Lemma measurable_gen_ext :
-  forall genE',
-    Incl genE (measurable genE') -> Incl genE' (measurable genE) ->
-    measurable genE = measurable genE'.
-Proof.
-apply Sigma_algebra_ext.
-Qed.
-
-Lemma measurable_gen_remove :
-  forall A, measurable genE A ->
-    Incl (measurable (add genE A)) (measurable genE).
-Proof.
-apply Sigma_algebra_gen_remove.
-Qed.
-
-Lemma measurable_gen_remove_alt :
-  forall A, measurable genE A -> Incl (add genE A) (measurable genE).
-Proof.
-apply Sigma_algebra_gen_remove_alt.
-Qed.
-
-Lemma measurable_gen_remove_full :
-  Incl (add genE fullset) (measurable genE).
-Proof.
-apply Sigma_algebra_gen_remove_full.
-Qed.
-
-Lemma measurable_gen_add_eq :
-  forall A, measurable genE A -> measurable (add genE A) = measurable genE.
-Proof.
-apply Sigma_algebra_gen_add_eq.
-Qed.
-
-End measurable_gen_Facts1.
-
-
-Section measurable_gen_Image_Def.
-
-Context {E F : Type}. (* Universes. *)
-
-Variable f : E -> F.
-Variable PE : (E -> Prop) -> Prop. (* Subset system. *)
-Variable PF : (F -> Prop) -> Prop. (* Subset system. *)
-
-(* From Lemma 524 p. 93 (v2) *)
-Definition Image : (F -> Prop) -> Prop := fun B => PE (preimage f B).
-
-(* From Lemma 523 p. 93 (v2) *)
-Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
-
-End measurable_gen_Image_Def.
-
-
-Section measurable_gen_Image_Facts.
-
-Context {E F : Type}. (* Universes. *)
-
-Variable f : E -> F.
-
-Lemma Image_monot :
-  forall PE1 PE2, Incl PE1 PE2 -> Incl (Image f PE1) (Image f PE2).
-Proof.
-intros PE1 PE2 H B HB; apply H; easy.
-Qed.
-
-Lemma Preimage_monot :
-  forall PF1 PF2, Incl PF1 PF2 -> Incl (Preimage f PF1) (Preimage f PF2).
-Proof.
-apply image_monot.
-Qed.
-
-Lemma Preimage_of_Image : forall PE, Incl (Preimage f (Image f PE)) PE.
-Proof.
-intros PE A [B HB]; easy.
-Qed.
-
-Lemma Image_of_Preimage : forall PF, Incl PF (Image f (Preimage f PF)).
-Proof.
-easy.
-Qed.
-
-Lemma Incl_Image_Preimage_Incl :
-  forall PE PF, Incl PF (Image f PE) -> Incl (Preimage f PF) PE.
-Proof.
-intros PE PF H; apply Incl_trans with (Preimage f (Image f PE)).
-apply Preimage_monot; easy.
-apply Preimage_of_Image.
-Qed.
-
-Lemma Preimage_Incl_Incl_Image :
-  forall PE PF, Incl (Preimage f PF) PE -> Incl PF (Image f PE).
-Proof.
-intros PE PF H; apply Incl_trans with (Image f (Preimage f PF)).
-apply Image_of_Preimage.
-apply Image_monot; easy.
-Qed.
-
-End measurable_gen_Image_Facts.
-
-
-Section measurable_gen_Image_Facts2.
-
-Context {E F : Type}. (* Universes. *)
-Variable genE : (E -> Prop) -> Prop. (* Generator. *)
-Variable genF : (F -> Prop) -> Prop. (* Generator. *)
-
-Variable f : E -> F.
-
-(* From Lemma 524 p. 93 (v2) *)
-Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE)).
-Proof.
-apply Sigma_algebra_equiv; repeat split.
-apply measurable_empty.
-intros B HB; apply measurable_compl; easy.
-intros B HB; apply measurable_union_seq; easy.
-Qed.
-
-(* From Lemma 523 p. 93 (v2) *)
-Lemma is_Sigma_algebra_Preimage :
-  is_Sigma_algebra (Preimage f (measurable genF)).
-Proof.
-apply Sigma_algebra_equiv; repeat split.
-(* *)
-unfold wEmpty(*, Preimage*).
-rewrite <- (preimage_emptyset f).
-
-
-exists emptyset; split.
-apply measurable_empty.
-symmetry; apply preimage_emptyset.
-(* *)
-intros A [B HB]; exists (compl B); split.
-apply measurable_compl; easy.
-rewrite preimage_compl; f_equal; easy.
-(* *)
-intros A HA.
-destruct (choice
-    (fun n Bn => measurable genF Bn /\ A n = preimage f Bn) HA) as [B HB].
-exists (union_seq B); split.
-apply measurable_union_seq; intros n; apply HB.
-rewrite preimage_union_seq_distr; f_equal.
-apply subset_seq_ext.
-intros n; rewrite (proj2 (HB n)); easy.
-Qed.
-
-End measurable_gen_Image_Facts2.
-
-
-Section measurable_gen_Image_Facts3.
-
-Context {E F : Type}. (* Universes. *)
-Variable genE : (E -> Prop) -> Prop. (* Generator. *)
-Variable genF : (F -> Prop) -> Prop. (* Generator. *)
-
-Variable f : E -> F.
-
-(* Lemma 527 pp. 93-94 (v2) *)
-Lemma measurable_gen_Preimage :
-  measurable (Preimage f genF) = Preimage f (measurable genF).
-Proof.
-apply Ext_equiv; split.
-(* *)
-rewrite <- is_Sigma_algebra_Preimage.
-apply measurable_gen_monot, Preimage_monot, measurable_gen.
-(* *)
-apply Incl_Image_Preimage_Incl, measurable_gen_lub_alt.
-apply is_Sigma_algebra_Image.
-apply Preimage_Incl_Incl_Image, measurable_gen.
-Qed.
-
-End measurable_gen_Image_Facts3.
-
-
-Section measurable_subspace.
-
-Context {E : Type}. (* Universe. *)
-
-Variable P : (E -> Prop) -> Prop. (* Subset system. *)
-
-Lemma measurable_subspace :
-  forall F, is_Sigma_algebra P -> is_Sigma_algebra (Trace P F).
-Proof.
-intros F; rewrite 2!Sigma_algebra_equiv; intros HP; repeat split.
-(* *)
-apply Trace_wEmpty; easy.
-(* *)
-
-
-
-Admitted.
-
-End measurable_subspace.
-
-
-Section Cartesian_product_def.
-
-Context {E1 E2 : Type}. (* Universes. *)
-Variable genE1 : (E1 -> Prop) -> Prop. (* Generator. *)
-Variable genE2 : (E2 -> Prop) -> Prop. (* Generator. *)
-
-Definition Prod_measurable : (E1 * E2 -> Prop) -> Prop :=
-  Prod (measurable genE1) (measurable genE2).
-
-Definition measurable_Prod : (E1 * E2 -> Prop) -> Prop :=
-  measurable Prod_measurable.
-
-End Cartesian_product_def.
-
-
-Section Cartesian_product_Facts1.
-
-Context {E1 E2 : Type}. (* Universe. *)
-Variable genE1 : (E1 -> Prop) -> Prop. (* Generator. *)
-Variable genE2 : (E2 -> Prop) -> Prop. (* Generator. *)
-
-Let genE1xE2 := Gen_Prod genE1 genE2.
-Let genE2xE1 := Gen_Prod genE2 genE1.
-
-(* From Lemma 542 p. 98 (case m := 2) *)
-Lemma measurable_prod_alt :
-  forall A1 A2, measurable genE1 A1 -> measurable genE2 A2 ->
-    measurable_Prod genE1 genE2 (prod A1 A2).
-Proof.
-apply Sigma_algebra_prod_alt.
-Qed.
-
-Lemma measurable_prod :
-  forall A1 A2, measurable genE1 A1 -> measurable genE2 A2 ->
-    measurable genE1xE2 (prod A1 A2).
-Proof.
-apply Sigma_algebra_prod.
-Qed.
-
-Lemma measurable_Prod_eq :
-   measurable_Prod genE1 genE2 = measurable genE1xE2.
-Proof.
-apply Sigma_algebra_Prod_eq.
-Qed.
-
-Lemma measurable_swap :
-  forall A, measurable genE1xE2 A -> measurable genE2xE1 (swap A).
-Proof.
-apply Sigma_algebra_swap.
-Qed.
-
-Lemma measurable_swap_rev :
-  forall A, measurable genE2xE1 (swap A) -> measurable genE1xE2 A.
-Proof.
-apply Sigma_algebra_swap_rev.
-Qed.
-
-Lemma measurable_swap_equiv :
-  forall A, measurable genE1xE2 A <-> measurable genE2xE1 (swap A).
-Proof.
-apply Sigma_algebra_swap_equiv.
-Qed.
-
-End Cartesian_product_Facts1.
-
-
-Section Cartesian_product_Facts2.
-
-Context {E F : Type}. (* Universe. *)
-Variable genE1 genE2 : (E -> Prop) -> Prop. (* Generator. *)
-Variable genF1 genF2 : (F -> Prop) -> Prop. (* Generator. *)
-
-Let genE1xF1 := Gen_Prod genE1 genF1.
-Let genE2xF2 := Gen_Prod genE2 genF2.
-
-Lemma measurable_Gen_Prod_ext :
-  measurable genE1 = measurable genE2 ->
-  measurable genF1 = measurable genF2 ->
-  measurable genE1xF1 = measurable genE2xF2.
-Proof.
-apply Sigma_algebra_Gen_Prod_ext.
-Qed.
-
-End Cartesian_product_Facts2.
-
-
-Section Borel_subsets.
-
-Context {E : UniformSpace}. (* Uniform universe. *)
-
-(* Definition 517 p. 91 (v2) *)
-Definition measurable_Borel := measurable (@open E).
-
-(* From Lemma 518 p. 91 *)
-Lemma measurable_Borel_open : Incl open measurable_Borel.
-Proof.
-intros A HA; now apply measurable_gen.
-Qed.
-
-(* From Lemma 518 p. 91 *)
-Lemma measurable_Borel_closed : Incl closed measurable_Borel.
-Proof.
-intros A HA; now apply measurable_compl_rev, measurable_gen, open_not.
-Qed.
-
-Lemma measurable_Borel_equiv : measurable_Borel = measurable closed.
-Proof.
-apply Ext_equiv; split; apply measurable_gen_lub.
-intros A HA; now apply measurable_compl_rev, measurable_gen, closed_not.
-apply measurable_Borel_closed.
-Qed.
-
-(* Lemma 519 pp. 91-92 *)
-Lemma measurable_Borel_gen_ext :
-  forall genE,
-    Incl genE open -> Incl open (Union_seq_closure genE) ->
-    measurable_Borel = measurable genE.
-Proof.
-intros genE H1 H2; apply measurable_gen_ext.
-intros A HA; destruct (H2 A HA) as [B [HB1 HB2]].
-rewrite HB2; apply measurable_union_seq; intros n; apply measurable_gen, HB1.
-apply Incl_trans with open; now try apply measurable_gen.
-Qed.
-
-End Borel_subsets.
-
-
-Section Borel_Cartesian_product.
-
-Context {E F : UniformSpace}. (* Uniform universes. *)
-
-Let genExF := Gen_Prod (@open E) (@open F).
-
-(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
-Lemma measurable_Borel_prod_incl : Incl (measurable genExF) measurable_Borel.
-Proof.
-apply measurable_gen_monot.
-intros A [A1 [A2 [HA1 [HA2 HA]]]]; rewrite HA; apply open_prod.
-destruct HA1 as [HA1 | HA1]; try easy; rewrite HA1; apply open_true.
-destruct HA2 as [HA2 | HA2]; try easy; rewrite HA2; apply open_true.
-Qed.
-
-End Borel_Cartesian_product.
-
-
-Section Borel_Cartesian_product.
-
-Context {K1 K2 : AbsRing}.
-Let E1 := AbsRing_UniformSpace K1.
-Let E2 := AbsRing_UniformSpace K2.
-
-Let genE1xE2 := Gen_Prod (@open E1) (@open E2).
-
-Hypothesis HE1 : is_second_countable E1.
-Hypothesis HE2 : is_second_countable E2.
-
-(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
-Lemma measurable_Borel_prod_incl_alt :
-  Incl measurable_Borel (measurable genE1xE2).
-Proof.
-destruct HE1 as [B1 HB1], HE2 as [B2 HB2].
-generalize (topo_basis_Prod_correct B1 B2 HB1 HB2); intros [HBa HBb].
-destruct HB1 as [HB1 _], HB2 as [HB2 _].
-apply measurable_gen_lub.
-intros A HA; destruct (HBb A HA) as [P HP].
-apply measurable_ext with
-    (union_seq (fun n => inter (Prop_cst (P n)) (topo_basis_Prod B1 B2 n))).
-intros x; rewrite HP; easy.
-apply measurable_union_seq.
-intros n; apply measurable_inter.
-apply measurable_Prop.
-apply measurable_prod; apply measurable_gen; easy.
-Qed.
-
-(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
-Lemma measurable_Borel_prod_eq : measurable_Borel = measurable genE1xE2.
-Proof.
-intros; apply Ext_equiv; split.
-apply measurable_Borel_prod_incl_alt; easy.
-apply measurable_Borel_prod_incl.
-Qed.
-
-(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
-Lemma measurable_Borel_prod_eq_alt :
-  measurable_Borel = measurable_Prod (@open E1) (@open E2).
-Proof.
-rewrite measurable_Borel_prod_eq, measurable_Prod_eq; easy.
-Qed.
-
-End Borel_Cartesian_product.
diff --git a/Lebesgue/measurable.v b/Lebesgue/measurable.v
index be163e130c1c96e614473c4637566295e76fc0ed..a3999116fe0c8de5dc8ff3690a5bf75a887f92e0 100644
--- a/Lebesgue/measurable.v
+++ b/Lebesgue/measurable.v
@@ -248,61 +248,61 @@ End measurable_gen_Facts1.
 
 Section measurable_gen_Image_Def.
 
-Context {E F : Type}. (* Universes. *)
+Context {E1 E2 : Type}. (* Universes. *)
 
-Variable f : E -> F.
-Variable PE : (E -> Prop) -> Prop. (* Subset system. *)
-Variable PF : (F -> Prop) -> Prop. (* Subset system. *)
+Variable f : E1 -> E2.
+Variable P1 : (E1 -> Prop) -> Prop. (* Subset system. *)
+Variable P2 : (E2 -> Prop) -> Prop. (* Subset system. *)
 
 (* From Lemma 524 p. 93 (v2) *)
-Definition Image : (F -> Prop) -> Prop := fun B => PE (preimage f B).
+Definition Image : (E2 -> Prop) -> Prop := fun A2 => P1 (preimage f A2).
 
 (* From Lemma 523 p. 93 (v2) *)
-Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
+Definition Preimage : (E1 -> Prop) -> Prop := image (preimage f) P2.
 
 End measurable_gen_Image_Def.
 
 
 Section measurable_gen_Image_Facts.
 
-Context {E F : Type}. (* Universes. *)
+Context {E1 E2 : Type}. (* Universes. *)
 
-Variable f : E -> F.
+Variable f : E1 -> E2.
 
 Lemma Image_monot :
-  forall PE1 PE2, Incl PE1 PE2 -> Incl (Image f PE1) (Image f PE2).
+  forall P1 Q1, Incl P1 Q1 -> Incl (Image f P1) (Image f Q1).
 Proof.
-intros PE1 PE2 H B HB; apply H; easy.
+intros P1 Q1 H A2 HA2; apply H; easy.
 Qed.
 
 Lemma Preimage_monot :
-  forall PF1 PF2, Incl PF1 PF2 -> Incl (Preimage f PF1) (Preimage f PF2).
+  forall P2 Q2, Incl P2 Q2 -> Incl (Preimage f P2) (Preimage f Q2).
 Proof.
 apply image_monot.
 Qed.
 
-Lemma Preimage_of_Image : forall PE, Incl (Preimage f (Image f PE)) PE.
+Lemma Preimage_of_Image : forall P1, Incl (Preimage f (Image f P1)) P1.
 Proof.
-intros PE A [B [HB1 HB2]]; rewrite HB2; easy.
+intros P1 A1 [A2 HA2]; easy.
 Qed.
 
-Lemma Image_of_Preimage : forall PF, Incl PF (Image f (Preimage f PF)).
+Lemma Image_of_Preimage : forall P2, Incl P2 (Image f (Preimage f P2)).
 Proof.
-intros PF B HB; exists B; easy.
+easy.
 Qed.
 
 Lemma Incl_Image_Preimage_Incl :
-  forall PE PF, Incl PF (Image f PE) -> Incl (Preimage f PF) PE.
+  forall P1 P2, Incl P2 (Image f P1) -> Incl (Preimage f P2) P1.
 Proof.
-intros PE PF H; apply Incl_trans with (Preimage f (Image f PE)).
+intros P1 P2 H; apply Incl_trans with (Preimage f (Image f P1)).
 apply Preimage_monot; easy.
 apply Preimage_of_Image.
 Qed.
 
 Lemma Preimage_Incl_Incl_Image :
-  forall PE PF, Incl (Preimage f PF) PE -> Incl PF (Image f PE).
+  forall P1 P2, Incl (Preimage f P2) P1 -> Incl P2 (Image f P1).
 Proof.
-intros PE PF H; apply Incl_trans with (Image f (Preimage f PF)).
+intros P1 P2 H; apply Incl_trans with (Image f (Preimage f P2)).
 apply Image_of_Preimage.
 apply Image_monot; easy.
 Qed.
@@ -312,43 +312,40 @@ End measurable_gen_Image_Facts.
 
 Section measurable_gen_Image_Facts2.
 
-Context {E F : Type}. (* Universes. *)
-Variable genE : (E -> Prop) -> Prop. (* Generator. *)
-Variable genF : (F -> Prop) -> Prop. (* Generator. *)
+Context {E1 E2 : Type}. (* Universes. *)
+Variable genE1 : (E1 -> Prop) -> Prop. (* Generator. *)
+Variable genE2 : (E2 -> Prop) -> Prop. (* Generator. *)
 
-Variable f : E -> F.
+Variable f : E1 -> E2.
 
 (* From Lemma 524 p. 93 (v2) *)
-Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE)).
+Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE1)).
 Proof.
 apply Sigma_algebra_equiv; repeat split.
 apply measurable_empty.
-intros B HB; apply measurable_compl; easy.
-intros B HB; apply measurable_union_seq; easy.
+intros A2 HA2; apply measurable_compl; easy.
+intros A2 HA2; apply measurable_union_seq; easy.
 Qed.
 
 (* From Lemma 523 p. 93 (v2) *)
 Lemma is_Sigma_algebra_Preimage :
-  is_Sigma_algebra (Preimage f (measurable genF)).
+  is_Sigma_algebra (Preimage f (measurable genE2)).
 Proof.
 apply Sigma_algebra_equiv; repeat split.
 (* *)
-exists emptyset; split.
-apply measurable_empty.
-symmetry; apply preimage_emptyset.
+unfold wEmpty; rewrite <- (preimage_emptyset f).
+apply Im, measurable_empty.
 (* *)
-intros A [B HB]; exists (compl B); split.
-apply measurable_compl; easy.
-rewrite preimage_compl; f_equal; easy.
+intros A1 [A2 HA2]; rewrite <- preimage_compl.
+apply Im, measurable_compl; easy.
 (* *)
-intros A HA.
-destruct (choice
-    (fun n Bn => measurable genF Bn /\ A n = preimage f Bn) HA) as [B HB].
-exists (union_seq B); split.
-apply measurable_union_seq; intros n; apply HB.
-rewrite preimage_union_seq_distr; f_equal.
-apply subset_seq_ext.
-intros n; rewrite (proj2 (HB n)); easy.
+intros A1 HA1; unfold Preimage in *; rewrite image_eq in HA1.
+destruct (choice (fun n A2 =>
+    measurable genE2 A2 /\ A1 n = preimage f A2) HA1) as [A2 HA2].
+assert (H : union_seq A1 = preimage f (union_seq A2)).
+  rewrite preimage_union_seq_distr; f_equal.
+  apply subset_seq_ext; intros n; rewrite (proj2 (HA2 n)); easy.
+rewrite H; apply Im; apply measurable_union_seq; intro; apply HA2.
 Qed.
 
 End measurable_gen_Image_Facts2.