diff --git a/_CoqProject b/_CoqProject
index 757942874..5c7d9647f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,7 +44,7 @@ theories/convex.v
 theories/charge.v
 theories/kernel.v
 theories/prob_lang.v
-theories/wip.v
+theories/prob_lang_wip.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v
diff --git a/theories/wip.v b/theories/prob_lang_wip.v
similarity index 99%
rename from theories/wip.v
rename to theories/prob_lang_wip.v
index 684c1806d..7b12eed1b 100644
--- a/theories/wip.v
+++ b/theories/prob_lang_wip.v
@@ -75,7 +75,7 @@ Let mgauss01_sigma_additive : semi_sigma_additive mgauss01.
 Proof.
 move=> /= F mF tF mUF.
 rewrite /mgauss01/= integral_bigcup//=; last first.
-  split.
+  apply/integrableP; split.
     apply/EFin_measurable_fun.
     exact: measurable_funS (measurable_fun_gauss_density 0 1).
   rewrite (_ : (fun x => _) = (EFin \o gauss01_density)); last first.