diff --git a/Lebesgue/measurable.v b/Lebesgue/measurable.v
index a3999116fe0c8de5dc8ff3690a5bf75a887f92e0..8dc47e6b47ebdb505f83ebd8124c2318e48c3762 100644
--- a/Lebesgue/measurable.v
+++ b/Lebesgue/measurable.v
@@ -521,6 +521,11 @@ rewrite HB2; apply measurable_union_seq; intros n; apply measurable_gen, HB1.
 apply Incl_trans with open; now try apply measurable_gen.
 Qed.
 
+(* WIP.
+Lemma measurable_Borel_eq_topo_basis :
+  forall Idx B, @is_topo_basis E Idx B -> 
+*)
+
 End Borel_subsets.