diff --git a/Lebesgue/measurable.v b/Lebesgue/measurable.v
index 8cad828b87f3522329c7ab86aad66ce1f7743f1c..518d2f12254bff321b2102bdae8002f387cd047e 100644
--- a/Lebesgue/measurable.v
+++ b/Lebesgue/measurable.v
@@ -303,7 +303,7 @@ Qed.
 End measurable_gen_Image_Facts.
 
 
-Section measurable_gen_Facts2.
+Section measurable_gen_Image_Facts2.
 
 Context {E F : Type}. (* Universes. *)
 Variable genE : (E -> Prop) -> Prop. (* Generator. *)
@@ -343,10 +343,10 @@ apply subset_seq_ext.
 intros n; rewrite (proj2 (HB n)); easy.
 Qed.
 
-End measurable_gen_Facts2.
+End measurable_gen_Image_Facts2.
 
 
-Section measurable_gen_Facts3.
+Section measurable_gen_Image_Facts3.
 
 Context {E F : Type}. (* Universes. *)
 Variable genE : (E -> Prop) -> Prop. (* Generator. *)
@@ -367,7 +367,7 @@ apply is_Sigma_algebra_Image.
 apply Preimage_Incl_Incl_Image, measurable_gen.
 Qed.
 
-End measurable_gen_Facts3.
+End measurable_gen_Image_Facts3.
 
 
 Section measurable_correct.