diff --git a/Lebesgue/LInt.v b/Lebesgue/LInt.v
index cdb131cac75e676c6eca181df4b55bedf572aa30..878a4e1e4f0af9b2c21cec11988e62322b9f4ca6 100644
--- a/Lebesgue/LInt.v
+++ b/Lebesgue/LInt.v
@@ -31,7 +31,6 @@ Open Scope R_scope.
 Section LInt_def.
 
 Context {E : Set}.  (* was Type -- to be looked into *)
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -267,7 +266,7 @@ Lemma Bif_ex_LInt : forall (f : E -> R),
   unfold mult; simpl; ring.
   assert (T2: is_finite ((LInt_p mu (fun x => Rbar_abs (seq N x))))).
   generalize (integrable_sf_norm (ax_int N)).
-  intros K; generalize (Bif_integrable_sf ax_notempty K).
+  intros K; generalize (Bif_integrable_sf K).
   intros K'; generalize (is_finite_LInt_p_Bif K').
   unfold fun_Bif, fun_norm.
   intros Y.
@@ -289,14 +288,14 @@ Lemma Bif_ex_LInt : forall (f : E -> R),
   apply measurable_fun_opp.
   apply measurable_fun_R_Rbar.
   apply Bif_measurable.
-  apply Bif_integrable_sf; easy.
+  apply (Bif_integrable_sf (ax_int N)); easy.
   intros t; easy.
   split.
   intros x; apply Rbar_abs_ge_0.
   apply measurable_fun_abs.
   apply measurable_fun_R_Rbar.
   apply Bif_measurable.
-  apply Bif_integrable_sf; easy.
+  apply (Bif_integrable_sf (ax_int N)); easy.
 Qed.
 
 Lemma ex_LInt_Bif : forall (f : E -> R),
diff --git a/Lebesgue/LInt_p.v b/Lebesgue/LInt_p.v
index f359cb3248d250881f2c2150c28cfe78fc032271..9273c77d685956c6bcd391e14015fd413797ebd7 100644
--- a/Lebesgue/LInt_p.v
+++ b/Lebesgue/LInt_p.v
@@ -38,7 +38,6 @@ Require Import Mp.
 Section LInt_p_def.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -80,8 +79,7 @@ Qed.
 (* Lemma 793 p. 164 *)
 Lemma LInt_p_0 : LInt_p (fun _ => 0) = 0.
 Proof.
-inversion Einhab as [x0].
-rewrite <- (LInt_SFp_0 mu x0) at 1.
+rewrite <- (LInt_SFp_0 mu) at 1.
 apply LInt_p_SFp_eq.
 intros x; simpl; auto with real.
 Qed.
@@ -231,7 +229,6 @@ End LInt_p_def.
 Section About_Beppo_Levi.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -442,7 +439,6 @@ End About_Beppo_Levi.
 Section About_Beppo_Levi_back.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -483,7 +479,6 @@ End About_Beppo_Levi_back.
 Section Theo_Beppo_Levi.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -630,7 +625,6 @@ End Theo_Beppo_Levi.
 Section Adap_seq_prop.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -646,7 +640,7 @@ replace f with (fun x => Sup_seq (fun n : nat => phi n x)).
 2: apply functional_extensionality.
 2: intros x; apply is_sup_seq_unique.
 2: apply Y.
-apply (Beppo_Levi_alt Einhab mu phi).
+apply (Beppo_Levi_alt mu phi).
 intros n; split.
 apply Y.
 destruct (Y4 n) as (l,Hl).
@@ -672,7 +666,6 @@ End Adap_seq_prop.
 Section Adap_seq_prop2.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -700,7 +693,6 @@ End Adap_seq_prop2.
 Section LInt_p_plus_def.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -720,8 +712,8 @@ fold phif; intros Yf Zf.
 generalize (mk_adapted_seq_is_adapted_seq g Hg).
 generalize (mk_adapted_seq_SF g Hg).
 fold phig; intros Yg Zg.
-rewrite <- (LInt_p_with_adapted_seq Einhab mu f phif); try easy.
-rewrite <- (LInt_p_with_adapted_seq Einhab mu g phig); try easy.
+rewrite <- (LInt_p_with_adapted_seq mu f phif); try easy.
+rewrite <- (LInt_p_with_adapted_seq mu g phig); try easy.
 assert (Yfg: SF_seq gen (fun n x => phif n x + phig n x)).
 intros n; apply SF_plus; [apply Yf|apply Yg].
 assert (Zfg: is_adapted_seq (fun x : E => Rbar_plus (f x) (g x))
@@ -738,15 +730,15 @@ intros T; apply T; clear T; try apply Zf; try apply Zg.
 apply ex_Rbar_plus_ge_0; [apply Hf| apply Hg].
 rewrite <- Sup_seq_plus.
 (* *)
-rewrite <- LInt_p_with_adapted_seq with (2:=Zfg); try easy.
+rewrite <- LInt_p_with_adapted_seq with (1:=Zfg); try easy.
 apply Sup_seq_ext.
 intros n.
-rewrite LInt_p_SFp_eq with gen mu (phif n) (Yf n); try easy; try apply Zf.
-rewrite LInt_p_SFp_eq with gen mu (phig n) (Yg n); try easy; try apply Zg.
-rewrite LInt_p_SFp_eq with gen mu (fun x => phif n x + phig n x) (Yfg n);
+rewrite LInt_p_SFp_eq with mu (phif n) (Yf n); try easy; try apply Zf.
+rewrite LInt_p_SFp_eq with mu (phig n) (Yg n); try easy; try apply Zg.
+rewrite LInt_p_SFp_eq with mu (fun x => phif n x + phig n x) (Yfg n);
     try easy; try apply Zfg.
 erewrite LInt_SFp_correct; try apply Zfg.
-rewrite LInt_SFp_plus with gen mu (phif n) (Yf n) (phig n) (Yg n);
+rewrite LInt_SFp_plus with mu (phif n) (Yf n) (phig n) (Yg n);
   try easy; [ apply Zf | apply Zg].
 intros n; apply LInt_p_monotone; intros x; apply Zf.
 intros n; apply LInt_p_monotone; intros x; apply Zg.
@@ -1471,7 +1463,6 @@ End LInt_p_plus_def.
 Section LInt_p_mu_ext.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {genE : (E -> Prop) -> Prop}.
 Variable mu1 mu2 : measure genE.
@@ -1498,8 +1489,6 @@ End LInt_p_mu_ext.
 Section LInt_p_chg_meas.
 
 Context {E F : Type}.
-Hypothesis Einhab : inhabited E.
-Hypothesis Finhab : inhabited F.
 
 Context {genE : (E -> Prop) -> Prop}.
 Context {genF : (F -> Prop) -> Prop}.
@@ -1569,7 +1558,6 @@ End LInt_p_chg_meas.
 Section LInt_p_Dirac.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {genE : (E -> Prop) -> Prop}.
 
@@ -1584,7 +1572,7 @@ rewrite Sup_seq_ext with (v := fun n => mk_adapted_seq f n a).
 now rewrite <- (mk_adapted_seq_Sup _ Hf).
 intros.
 assert (Hphi : SF genE (mk_adapted_seq f n)) by now apply mk_adapted_seq_SF.
-rewrite (LInt_p_SFp_eq Einhab _ _ Hphi); try easy.
+rewrite (LInt_p_SFp_eq _ _ Hphi); try easy.
 apply LInt_SFp_Dirac.
 now apply (mk_adapted_seq_nonneg _ Hf).
 Qed.
diff --git a/Lebesgue/Mp.v b/Lebesgue/Mp.v
index 573bc3e76c137adcd23fde28317a922ac8b0d674..4182ec3bd7bec771bb60a94f59f216400fa2580e 100644
--- a/Lebesgue/Mp.v
+++ b/Lebesgue/Mp.v
@@ -16,7 +16,7 @@ COPYING file for more details.
 
 (** Inductive types for SFplus and Mplus. *)
 
-From Coq Require Import FunctionalExtensionality.
+From Coq Require Import FunctionalExtensionality Classical.
 From Coq Require Import Reals List.
 From Coquelicot Require Import Coquelicot.
 
@@ -32,7 +32,6 @@ Section SFp_def.
 (** Inductive type for SFplus. *)
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Variable gen : (E -> Prop) -> Prop.
 
@@ -50,7 +49,8 @@ Qed.
 
 Lemma SFplus_is_SFp : forall f : E -> R, SFplus gen f -> SFp f.
 Proof.
-destruct Einhab as [x0].
+case (classic (inhabited E)); intros Y.
+destruct Y as [ x0 ].
 intros f [Hf1 [l Hf2]].
 generalize l f Hf1 Hf2; clear l f Hf1 Hf2.
 intros l; case l.
@@ -85,6 +85,13 @@ apply Raux.Rle_0_minus, Rlt_le; destruct Hf2 as [[Hf2 _] _]; now inversion Hf2.
 apply SFp_charac.
 apply Hf2.
 now apply IHl with v1.
+(* *)
+intros f H.
+eapply SFp_ext.
+2: apply SFp_charac.
+2: apply measurable_empty.
+intros x.
+contradict Y; easy.
 Qed.
 
 Lemma SFp_is_SFplus : forall f, SFp f -> SFplus gen f.
@@ -124,7 +131,6 @@ Section Mp1_def.
 (** First inductive type for Mplus based on SFp and real-valued functions. *)
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Variable gen : (E -> Prop) -> Prop.
 
@@ -174,7 +180,6 @@ Section Mp2_def.
 (** Second inductive type for Mplus based on real-valued functions. *)
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Variable gen : (E -> Prop) -> Prop.
 
@@ -239,7 +244,6 @@ Section Mp_def.
 (** Third inductive type for Mplus based on extended real-valued functions. *)
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Variable gen : (E -> Prop) -> Prop.
 
diff --git a/Lebesgue/Tonelli.v b/Lebesgue/Tonelli.v
index d36b0fc570a7c56b3e386c5f66b4dd624538505a..dbf24eefbf324489cdb9af027d2c6e4189b14d9f 100644
--- a/Lebesgue/Tonelli.v
+++ b/Lebesgue/Tonelli.v
@@ -447,7 +447,6 @@ Section Product_Measure_Def.
 (** Definition of the product measure. *)
 
 Context {X1 X2 : Type}.
-Hypothesis IX1: inhabited X1.
 
 Context {genX1 : (X1 -> Prop) -> Prop}.
 Context {genX2 : (X2 -> Prop) -> Prop}.
@@ -779,8 +778,6 @@ Section Integral_Of_Section_Fun_Facts.
 (** Definition and properties of the integral of sections of functions. *)
 
 Context {X1 X2 : Type}.
-Hypothesis IX1: inhabited X1.
-Hypothesis IX2: inhabited X2.
 
 Context {genX1 : (X1 -> Prop) -> Prop}.
 Context {genX2 : (X2 -> Prop) -> Prop}.
@@ -902,8 +899,6 @@ Section Iterated_Integrals_Facts.
  ie the integral of the integral of sections of functions. *)
 
 Context {X1 X2 : Type}.
-Hypothesis IX1: inhabited X1.
-Hypothesis IX2: inhabited X2.
 
 Context {genX1 : (X1 -> Prop) -> Prop}.
 Context {genX2 : (X2 -> Prop) -> Prop}.
@@ -919,7 +914,7 @@ Definition iterated_integrals : (X1 * X2 -> Rbar) -> Rbar :=
   fun f => LInt_p muX1 (LInt_p_section_fun muX2 f).
 *)
 
-Let muX1xX2 := meas_prod IX1 muX1 muX2 HmuX2.
+Let muX1xX2 := meas_prod muX1 muX2 HmuX2.
 
 Lemma P_ext :
   forall {X : Type} (P : (X -> Rbar) -> Prop) f1 f2,
@@ -939,7 +934,6 @@ Proof.
 intros A HA; split.
 now apply LInt_p_section_fun_Mplus_charac.
 rewrite LInt_p_charac; try easy.
-2: now apply inhabited_prod.
 apply LInt_p_ext; intros.
 erewrite <- LInt_p_section_fun_charac; try easy; apply HA.
 Qed.
@@ -954,7 +948,6 @@ now apply LInt_p_section_fun_Mplus_scal.
 rewrite (LInt_p_ext muX1) with
     (g := fun x1 => Rbar_mult a (LInt_p_section_fun muX2 f x1)).
 rewrite 2!LInt_p_scal, Hf3; try easy.
-now apply inhabited_prod.
 intros; eapply LInt_p_section_fun_scal; now try apply Hf1.
 Qed.
 
@@ -969,7 +962,6 @@ rewrite (LInt_p_ext muX1) with
   (g := fun x1 =>
     Rbar_plus (LInt_p_section_fun muX2 f x1) (LInt_p_section_fun muX2 g x1)).
 rewrite 2!LInt_p_plus, Hf3, Hg3; try easy.
-now apply inhabited_prod.
 intros; eapply LInt_p_section_fun_plus; try apply Hf1; now try apply Hg1.
 Qed.
 
@@ -986,7 +978,6 @@ rewrite 2!Beppo_Levi; try easy.
 apply Sup_seq_ext, Hf3.
 intros n; apply Hf3.
 intros x1 n; apply LInt_p_section_fun_monot; intros x; apply Hf2.
-now apply inhabited_prod.
 intros; eapply LInt_p_section_fun_Sup_seq; now try apply Hf1.
 Qed.
 
@@ -998,8 +989,6 @@ Section Tonelli_aux1.
 (** First formula of the Tonelli theorem. *)
 
 Context {X1 X2 : Type}.
-Hypothesis IX1: inhabited X1.
-Hypothesis IX2: inhabited X2.
 
 Context {genX1 : (X1 -> Prop) -> Prop}.
 Context {genX2 : (X2 -> Prop) -> Prop}.
@@ -1010,7 +999,7 @@ Variable muX1 : measure genX1.
 Variable muX2 : measure genX2.
 Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.
 
-Let muX1xX2 := meas_prod IX1 muX1 muX2 HmuX2.
+Let muX1xX2 := meas_prod muX1 muX2 HmuX2.
 
 (* From Theorem 846 pp. 182-183. *)
 Lemma Tonelli_aux1 :
@@ -1018,7 +1007,6 @@ Lemma Tonelli_aux1 :
     Mplus genX1 (LInt_p_section_fun muX2 f) /\
     LInt_p muX1xX2 f = LInt_p muX1 (LInt_p_section_fun muX2 f).
 Proof.
-assert (IX1xX2: inhabited (X1 * X2)) by now apply inhabited_prod.
 intros f Hf.
 apply Mp_correct in Hf; try easy.
 induction Hf.
@@ -1036,8 +1024,6 @@ Section Tonelli_aux2.
 (** Second formula of the Tonelli theorem. *)
 
 Context {X1 X2 : Type}.
-Hypothesis IX1: inhabited X1.
-Hypothesis IX2: inhabited X2.
 
 Context {genX1 : (X1 -> Prop) -> Prop}.
 Context {genX2 : (X2 -> Prop) -> Prop}.
@@ -1050,8 +1036,8 @@ Variable muX2 : measure genX2.
 Hypothesis HmuX1 : is_sigma_finite_measure genX1 muX1.
 Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.
 
-Let muX1xX2 : measure genX1xX2 := meas_prod IX1 muX1 muX2 HmuX2.
-Let muX2xX1 : measure genX2xX1 := meas_prod IX2 muX2 muX1 HmuX1.
+Let muX1xX2 : measure genX1xX2 := meas_prod muX1 muX2 HmuX2.
+Let muX2xX1 : measure genX2xX1 := meas_prod muX2 muX1 HmuX1.
 
 Let meas_prod_swap : measure genX1xX2 := meas_image _ measurable_fun_swap_var muX2xX1.
 
@@ -1059,7 +1045,7 @@ Lemma meas_prod_swap_is_product_measure :
   is_product_measure muX1 muX2 meas_prod_swap.
 Proof.
 intros A1 A2 HA1 HA2; rewrite Rbar_mult_comm.
-rewrite <- (meas_prod_is_product_measure IX2 _ _ HmuX1); try easy.
+rewrite <- (meas_prod_is_product_measure _ _ HmuX1); try easy.
 unfold meas_prod_swap; simpl.
 f_equal; now rewrite <- (prod_swap A1 A2).
 Qed.
@@ -1071,7 +1057,7 @@ Lemma Tonelli_aux2 :
     LInt_p muX1xX2 f = LInt_p muX2 (LInt_p_section_fun muX1 (swap f)).
 Proof.
 intros f Hf.
-destruct (Tonelli_aux1 IX2 IX1 muX2 _ HmuX1 (swap f)) as [Y1 Y2]; try easy.
+destruct (Tonelli_aux1 muX2 _ HmuX1 (swap f)) as [Y1 Y2]; try easy.
 now apply Mplus_swap.
 split; try easy.
 rewrite <- Y2.
@@ -1081,7 +1067,7 @@ intros A HA; unfold meas_prod.
 apply meas_prod_uniqueness_sigma_finite with muX1 muX2; try easy.
 apply meas_prod_is_product_measure.
 apply meas_prod_swap_is_product_measure.
-unfold swap; apply LInt_p_change_meas; now try apply inhabited_prod.
+unfold swap; apply LInt_p_change_meas; easy.
 Qed.
 
 End Tonelli_aux2.
@@ -1092,8 +1078,6 @@ Section Tonelli.
 (** The Tonelli theorem. *)
 
 Context {X1 X2 : Type}.
-Hypothesis IX1: inhabited X1.
-Hypothesis IX2: inhabited X2.
 
 Context {genX1 : (X1 -> Prop) -> Prop}.
 Context {genX2 : (X2 -> Prop) -> Prop}.
@@ -1105,7 +1089,7 @@ Variable muX2 : measure genX2.
 Hypothesis HmuX1 : is_sigma_finite_measure genX1 muX1.
 Hypothesis HmuX2 : is_sigma_finite_measure genX2 muX2.
 
-Let muX1xX2 := meas_prod IX1 muX1 muX2 HmuX2.
+Let muX1xX2 := meas_prod muX1 muX2 HmuX2.
 
 (* Theorem 846 pp. 182-183 *)
 Theorem Tonelli :
diff --git a/Lebesgue/bochner_integral/BInt_Bif.v b/Lebesgue/bochner_integral/BInt_Bif.v
index 6dc9377193b30265167a4c50f5b6f8f24fbad8b8..f5f10bcf70dc7514503d039ba5e026be85e738e8 100644
--- a/Lebesgue/bochner_integral/BInt_Bif.v
+++ b/Lebesgue/bochner_integral/BInt_Bif.v
@@ -95,8 +95,8 @@ Section BInt_prop.
             BInt bf = BInt bf'.
     Proof.
         move => bf bf' Ext;
-            case_eq bf => s ι ints Hspw Hsl1 Eqπ;
-            case_eq bf' => s' ι' ints' Hs'pw Hs'l1 Eqπ';
+            case_eq bf => s ints Hspw Hsl1 Eqπ;
+            case_eq bf' => s' ints' Hs'pw Hs'l1 Eqπ';
             unfold BInt => /=.
         pose I := lim_seq (λ n : nat, BInt_sf μ (s n));
         pose I' := lim_seq (λ n : nat, BInt_sf μ (s' n)).
@@ -181,7 +181,6 @@ Section BInt_prop.
             apply norm_Bint_sf_le.
         rewrite (BInt_sf_LInt_SFp).
         rewrite <-LInt_p_SFp_eq.
-            2 : exact ι.
             all : swap 1 2.
             unfold sum_Rbar_nonneg.nonneg => x /=.
             rewrite fun_sf_norm.
@@ -215,7 +214,6 @@ Section BInt_prop.
         rewrite (LInt_p_ext _ _ (λ x : X, Rbar_plus ((‖ f - s n ‖)%fn x) ((‖ f - s' n ‖)%fn x)%hy)).
             2 : by [].
         rewrite LInt_p_plus.
-            2 : exact ι.
             2, 3 : split.
             2, 4 : unfold sum_Rbar_nonneg.nonneg => x.
             2, 3 : unfold fun_norm; apply norm_ge_0.
@@ -240,7 +238,6 @@ Section BInt_prop.
         pose Lint_p_Bint_sf :=
             @Finite_BInt_sf_LInt_SFp _ _ μ (‖ s n - s' n ‖)%sf.
             rewrite <-LInt_p_SFp_eq in Lint_p_Bint_sf.
-            2 : exact ι.
             2 : unfold sum_Rbar_nonneg.nonneg => x.
             2 : simpl; rewrite fun_sf_norm.
             2 : apply norm_ge_0.
@@ -308,10 +305,10 @@ Section BInt_prop.
     Qed.
 
     Lemma BInt_BInt_sf {s : simpl_fun E gen} :
-        ∀ π : integrable_sf μ s, ∀ ι : inhabited X,
-        BInt_sf μ s = BInt (Bif_integrable_sf ι π).
+        ∀ π : integrable_sf μ s,
+        BInt_sf μ s = BInt (Bif_integrable_sf π).
     Proof.
-        move => π ι; unfold BInt; simpl.
+        move => π; unfold BInt; simpl.
         symmetry; apply: lim_seq_eq.
         apply lim_seq_cte.
     Qed.
@@ -323,7 +320,6 @@ Section BInt_indic.
 
     (* espace de départ *)
     Context {X : Set}.
-    Context (ι : inhabited X).
     (* espace d'arrivé *)
     Context {E : CompleteNormedModule R_AbsRing}.
     (* Un espace mesuré *)
@@ -332,7 +328,7 @@ Section BInt_indic.
 
     Lemma BInt_indic :
         ∀ P : X -> Prop, ∀ π : measurable gen P, ∀ π' : is_finite (μ P),
-            BInt (Bif_integrable_sf ι (integrable_sf_indic π π')) = μ P.
+            BInt (Bif_integrable_sf (integrable_sf_indic π π')) = μ P.
     Proof.
         move => P π π'.
         rewrite <-BInt_BInt_sf.
@@ -360,8 +356,8 @@ Section BInt_op.
             BInt (Bif_plus bf bg) = ((BInt bf) + (BInt bg))%hy.
     Proof.
         move => bf bg;
-        case_eq bf => sf ι isf Hfpw Hfl1 eqbf;
-        case_eq bg => sg ι' isg Hgpw Hgl1 eqbg;
+        case_eq bf => sf isf Hfpw Hfl1 eqbf;
+        case_eq bg => sg isg Hgpw Hgl1 eqbg;
         rewrite <-eqbf, <-eqbg.
         unfold BInt.
         apply lim_seq_eq.
@@ -370,10 +366,10 @@ Section BInt_op.
             rewrite eqbf eqbg => /=.
             rewrite BInt_sf_plus => //.
             apply: lim_seq_plus.
-            pose H := is_lim_seq_BInt (mk_Bif f sf ι isf Hfpw Hfl1);
+            pose H := is_lim_seq_BInt (mk_Bif f sf isf Hfpw Hfl1);
                 clearbody H; simpl in H; rewrite <-eqbf in H.
             assumption.
-            pose H := is_lim_seq_BInt (mk_Bif g sg ι' isg Hgpw Hgl1);
+            pose H := is_lim_seq_BInt (mk_Bif g sg isg Hgpw Hgl1);
                 clearbody H; simpl in H; rewrite <-eqbg in H.
             assumption.
     Qed.
@@ -383,12 +379,12 @@ Section BInt_op.
             BInt (Bif_scal a bf) = (a â‹… (BInt bf))%hy.
     Proof.
         move => bf a.
-        case: bf => sf ι isf Hfpw Hfl1.
+        case: bf => sf isf Hfpw Hfl1.
         apply lim_seq_eq.
         apply (lim_seq_ext (fun n : nat => a ⋅ (BInt_sf μ (sf n)))%hy).
             move => n; rewrite BInt_sf_scal => //.
             apply: lim_seq_scal_r.
-            pose H := is_lim_seq_BInt (mk_Bif f sf ι isf Hfpw Hfl1);
+            pose H := is_lim_seq_BInt (mk_Bif f sf isf Hfpw Hfl1);
                 clearbody H; simpl in H.
             assumption.
     Qed.
@@ -398,16 +394,16 @@ Section BInt_op.
             ‖ BInt bf ‖%hy <= BInt (‖bf‖)%Bif.
     Proof.
         move => bf.
-        case: bf => sf ι isf Hfpw Hfl1.
+        case: bf => sf isf Hfpw Hfl1.
         suff: (Rbar_le (‖ lim_seq (λ n : nat, BInt_sf μ (sf n)) ‖)%hy (lim_seq (λ n : nat, BInt_sf μ (‖ sf n ‖)%sf)))
             by simpl => //.
         apply is_lim_seq_le with (λ n : nat, ‖ BInt_sf μ (sf n) ‖)%hy (λ n : nat, BInt_sf μ (‖ sf n ‖%sf)).
             move => n; apply norm_Bint_sf_le.
             apply lim_seq_norm.
-            pose H := is_lim_seq_BInt (mk_Bif f sf ι isf Hfpw Hfl1);
+            pose H := is_lim_seq_BInt (mk_Bif f sf isf Hfpw Hfl1);
                 clearbody H; simpl in H.
             assumption.
-            pose H := is_lim_seq_BInt (Bif_norm (mk_Bif f sf ι isf Hfpw Hfl1));
+            pose H := is_lim_seq_BInt (Bif_norm (mk_Bif f sf isf Hfpw Hfl1));
                 clearbody H; simpl in H.
             assumption.
     Qed.
@@ -443,7 +439,7 @@ Section BInt_linearity.
             (∀ x : X, bf x = zero) -> BInt bf = zero.
     Proof.
         move => bf Hbf.
-        rewrite (BInt_ext bf (Bif_zero (ax_notempty bf))).
+        rewrite (BInt_ext bf (Bif_zero)).
         unfold Bif_zero.
         rewrite <-BInt_BInt_sf.
         unfold BInt_sf => /=.
diff --git a/Lebesgue/bochner_integral/BInt_LInt_p.v b/Lebesgue/bochner_integral/BInt_LInt_p.v
index ae96bce0d8550f10dd58f49ba57830d7daacde2a..15e3f279dfbf4aa848c51aa51dc892b3f49c7683 100644
--- a/Lebesgue/bochner_integral/BInt_LInt_p.v
+++ b/Lebesgue/bochner_integral/BInt_LInt_p.v
@@ -66,7 +66,6 @@ Section BInt_to_LInt_p.
 
     Lemma LInt_p_minus_le :
         ∀ f g : X -> R,
-        inhabited X ->
         measurable_fun_R gen f ->
         measurable_fun_R gen g ->
         (∀ x : X, 0 <= f x) ->
@@ -75,7 +74,7 @@ Section BInt_to_LInt_p.
         is_finite (LInt_p μ g) ->
             Rabs (LInt_p μ f - LInt_p μ g) <= LInt_p μ (fun x => Rabs (f x - g x)).
     Proof.
-        move => f g ι Hmeasf Hmeasg Hposf Hposg Hfinf Hfing.
+        move => f g Hmeasf Hmeasg Hposf Hposg Hfinf Hfing.
         assert (is_finite (LInt_p μ (λ x : X, Rabs (f x - g x)))) as finH1.
         apply: Rbar_bounded_is_finite.
         apply LInt_p_nonneg => //.
@@ -124,7 +123,6 @@ Section BInt_to_LInt_p.
         rewrite (LInt_p_ext _ _ (λ x : X, Rbar_plus (Rabs (f x - g x)) (f x))).
         rewrite LInt_p_plus.
         rewrite <-Hfinf, <-finH1 => //.
-        exact ι.
         1, 2 : split.
         move => x /=; apply Rabs_pos.
         apply measurable_fun_R_Rbar.
@@ -189,7 +187,6 @@ Section BInt_to_LInt_p.
         rewrite (LInt_p_ext _ _ (λ x : X, Rbar_plus (Rabs (f x - g x)) (g x))).
         rewrite LInt_p_plus.
         rewrite <-Hfing, <-finH1 => //.
-        exact ι.
         1, 2 : split.
         move => x /=; apply Rabs_pos.
         apply measurable_fun_R_Rbar.
@@ -294,7 +291,7 @@ Section BInt_to_LInt_p.
         BInt bf = LInt_p μ (bf : X -> R).
     Proof.
         move => bf.
-        case_eq bf => sf ι isf axfpw axfl1 /= Eqf axpos.
+        case_eq bf => sf isf axfpw axfl1 /= Eqf axpos.
         apply lim_seq_eq => /=.
         apply is_lim_seq_epsilon.
         move => É› HÉ›.
@@ -306,6 +303,7 @@ Section BInt_to_LInt_p.
         rewrite BInt_sf_plus.
         unfold sf_shifter.
         case: (sf_bounded (sf n)) => M HM.
+        destruct HM as (HM,HM').
         rewrite BInt_sf_scal.
         rewrite BInt_sf_indic.
         simpl.
@@ -319,7 +317,6 @@ Section BInt_to_LInt_p.
         unfold scal => /=.
         rewrite (LInt_p_ext _ _ (bf : X -> R)).
         2 : rewrite Eqf => //.
-        2, 4 : exact ι.
         rewrite <-(is_finite_LInt_p_Bif).
         2 : rewrite Eqf => //.
         simpl.
@@ -342,11 +339,7 @@ Section BInt_to_LInt_p.
         exact RIneq.Rle_0_1.
         apply RIneq.Rle_refl.
         all : swap 1 2.
-        case ι => x.
-        apply RIneq.Rle_trans with (‖ sf n x ‖).
-        apply norm_ge_0.
-        apply HM.
-        2 : exact ι.
+        simpl; easy.
         2, 3 : split.
         all : swap 1 2.
         move => x; apply axpos.
@@ -409,7 +402,6 @@ Section BInt_to_LInt_p.
         apply: finite_sf_preim_neq_0_alt.
         apply isf.
         rewrite <-LInt_p_SFp_eq.
-        2 : exact ι.
         all : swap 1 2.
         move => x /=.
         apply pos_shifted_sf.
@@ -422,7 +414,6 @@ Section BInt_to_LInt_p.
         unfold norm => /=.
         unfold abs => /=.
         apply LInt_p_minus_le.
-        exact ι.
         rewrite Eqss.
         suff: (measurable_fun gen open (sf n + sf_shifter (sf n))%sf).
         move => Hmeas P /measurable_R_equiv_oo/Hmeas//.
diff --git a/Lebesgue/bochner_integral/BInt_R.v b/Lebesgue/bochner_integral/BInt_R.v
index 67f3be479648551067f0b8b2850694d6a18d1497..e38f63b1a73b03a97daf0c28be5c6cb312b71223 100644
--- a/Lebesgue/bochner_integral/BInt_R.v
+++ b/Lebesgue/bochner_integral/BInt_R.v
@@ -112,7 +112,6 @@ Section BInt_R_prop.
         suff: Rbar_le 0 (LInt_p μ (λ x : X, bf x)).
         rewrite <-is_finite_LInt_p_Bif => //.
         apply LInt_p_nonneg.
-        exact (ax_notempty bf).
         move => x //=.
     Qed.
 
@@ -165,7 +164,6 @@ Section BInt_dominated_convergence_proof.
         exact (bf n).
         apply: Rbar_bounded_is_finite.
         apply LInt_p_nonneg.
-        1, 6 : exact (ax_notempty (bf O)).
         move => x; unfold fun_norm; apply norm_ge_0.
         2 : by [].
         all : swap 1 2.
@@ -271,7 +269,6 @@ Section BInt_dominated_convergence_proof.
             rewrite (LInt_p_ext _ _  (fun x => Rbar_mult 2 (g x))).
             2 : easy.
             rewrite LInt_p_scal => //.
-            2 : exact (ax_notempty blimf).
             all : swap 2 3.
             2 : split.
             2 : move => x /=.
@@ -286,7 +283,7 @@ Section BInt_dominated_convergence_proof.
             assumption.
 
         pose HCVD := LInt_p_dominated_convergence
-            (ax_notempty blimf) μ
+            μ
             (fun n => (‖ bf n - blimf ‖)%Bif : X -> R)
             (fun x => 2 * g x)
             H1_CVD
@@ -304,7 +301,6 @@ Section BInt_dominated_convergence_proof.
             rewrite <-CVD3.
             rewrite (LInt_p_ext _ _ (fun _ => 0)).
             rewrite LInt_p_0 => //.
-            exact (ax_notempty blimf).
             move => x.
             rewrite <-Lim_seq_eq.
             suff: Lim_seq.is_lim_seq (λ x0 : nat, (‖ bf x0 - blimf ‖)%fn x) 0.
diff --git a/Lebesgue/bochner_integral/B_spaces.v b/Lebesgue/bochner_integral/B_spaces.v
index 1d708e9fd98a7302c274880d3bde3a63bc19a75f..9f16efd04c9a382d38da125214bf30b546aca9c2 100644
--- a/Lebesgue/bochner_integral/B_spaces.v
+++ b/Lebesgue/bochner_integral/B_spaces.v
@@ -110,7 +110,6 @@ Section ae_eq_prop.
         suff: (LInt_p μ (λ x : X, (‖ bf ‖) x) = 0).
         move ->; apply RIneq.Rle_refl.
         apply LInt_p_ae_definite.
-        exact (ax_notempty bf).
         split.
         move => x; rewrite Bif_fn_norm; apply norm_ge_0.
         apply measurable_fun_R_Rbar.
@@ -229,7 +228,7 @@ Section ae_eq_prop2.
         assert (H : Mplus gen (λ x, ‖ bf ‖ x)).
             split => //.
         clear H_0 H_1.
-        case: (LInt_p_ae_definite (ax_notempty bf) μ (‖bf‖ : X -> R) H) => _ HypLInt_p.
+        case: (LInt_p_ae_definite μ (‖bf‖ : X -> R) H) => _ HypLInt_p.
         unfold ae_eq, ae_rel in HypLInt_p |- *.
         move: HInt0.
         rewrite BInt_LInt_p_eq; swap 1 2.
@@ -292,7 +291,6 @@ Section B_space_def.
         unfold abs at 1 => /=.
         rewrite Rabs_pos_eq => //.
         apply R_compl.Rpow_nonneg, norm_ge_0.
-        case: Hf => [_ [ι _]] //.
     Qed.
 
     Definition semi_norm_p (μ : measure gen) (p : posreal) {f : X -> E} (inBf : in_B_space μ p f) :=
diff --git a/Lebesgue/bochner_integral/Bi_fun.v b/Lebesgue/bochner_integral/Bi_fun.v
index b4df55cd96fa7ef06ae427fd426fe074979f7118..6461477e59e492efc0a2941a53d415d99d2b751e 100644
--- a/Lebesgue/bochner_integral/Bi_fun.v
+++ b/Lebesgue/bochner_integral/Bi_fun.v
@@ -170,7 +170,6 @@ Section Boshner_integrable_fun.
     Record Bif {f : X -> E} := mk_Bif {
         seq : nat -> simpl_fun E gen;
 
-        ax_notempty : inhabited X;
         ax_int : (∀ n : nat, integrable_sf μ (seq n));
         ax_lim_pw : (∀ x : X, is_lim_seq (fun n => seq n x) (f x));
         ax_lim_l1 : is_LimSup_seq_Rbar (fun n => LInt_p μ (‖ f - (seq n) ‖)%fn) 0
@@ -213,7 +212,7 @@ Section Bi_fun_prop.
     Lemma integrable_Bif {f : X -> E} :
         ∀ bf : Bif μ f, is_finite (LInt_p μ (‖ bf ‖)%fn).
     Proof.
-        case => sf ι isf axfpw axfl1 /=.
+        case => sf isf axfpw axfl1 /=.
         case: (axfl1 (RIneq.posreal_one)) => /=.
         move => H1 H2; case: H2 => N HN.
         rewrite Raxioms.Rplus_0_l in HN.
@@ -240,7 +239,6 @@ Section Bi_fun_prop.
         unfold fun_norm, fun_plus.
         unfold fun_scal; rewrite fun_sf_scal.
         apply: norm_triangle.
-        exact ι.
         1, 2 : split.
         all : swap 1 2.
         assert
@@ -284,7 +282,6 @@ Section Bi_fun_prop.
         all : swap 1 2.
         move => x; unfold fun_norm; rewrite fun_sf_norm => //.
         apply Rbar_le_refl.
-        exact ι.
         move => x; rewrite fun_sf_norm; apply norm_ge_0.
         apply integrable_sf_norm.
         apply isf.
@@ -293,11 +290,11 @@ Section Bi_fun_prop.
     Qed.
 
     Lemma Cauchy_seq_approx :
-        ∀ f : X -> E, ∀ s : nat -> simpl_fun E gen, (∀ n : nat, integrable_sf μ (s n)) -> inhabited X ->
+        ∀ f : X -> E, ∀ s : nat -> simpl_fun E gen, (∀ n : nat, integrable_sf μ (s n)) ->
             (∀ x : X, is_lim_seq (fun n => s n x) (f x)) -> is_LimSup_seq_Rbar (fun n => LInt_p μ (‖ f - (s n) ‖)%fn) 0
             -> NM_Cauchy_seq (fun n => BInt_sf μ (s n)).
     Proof.
-        move => f s isf ι Hspointwise Hs.
+        move => f s isf Hspointwise Hs.
         unfold Cauchy_seq => É› HÉ›.
         unfold is_LimSup_seq_Rbar in Hs.
         pose sighalfÉ› := RIneq.mkposreal (É› * /2) (R_compl.Rmult_lt_pos_pos_pos _ _ (RIneq.Rgt_lt _ _ HÉ›) RIneq.pos_half_prf).
@@ -313,7 +310,6 @@ Section Bi_fun_prop.
             apply norm_Bint_sf_le.
         rewrite (BInt_sf_LInt_SFp).
         rewrite <-LInt_p_SFp_eq.
-            2 : exact ι.
             all : swap 1 2.
             unfold sum_Rbar_nonneg.nonneg => x /=.
             rewrite fun_sf_norm.
@@ -348,7 +344,6 @@ Section Bi_fun_prop.
         rewrite (LInt_p_ext _ _ (λ x : X, Rbar_plus ((‖ f - s q ‖)%fn x) ((‖ f - s p ‖)%fn x)%hy)).
             2 : by [].
         rewrite LInt_p_plus.
-            2 : exact ι.
             2, 3 : split.
             2, 4 : unfold sum_Rbar_nonneg.nonneg => x.
             2, 3 : unfold fun_norm; apply norm_ge_0.
@@ -365,7 +360,6 @@ Section Bi_fun_prop.
         pose Lint_p_Bint_sf :=
             @Finite_BInt_sf_LInt_SFp _ _ μ (‖ s q - s p ‖)%sf.
             rewrite <-LInt_p_SFp_eq in Lint_p_Bint_sf.
-            2 : exact ι.
             2 : unfold sum_Rbar_nonneg.nonneg => x.
             2 : simpl; rewrite fun_sf_norm.
             2 : apply norm_ge_0.
@@ -440,7 +434,6 @@ Section Bif_sf.
 
     (* espace de départ *)
     Context {X : Set}.
-    Context (ι : inhabited X).
     (* espace d'arrivé *)
     Context {E : CompleteNormedModule R_AbsRing}.
     (* Un espace mesuré *)
@@ -453,7 +446,6 @@ Section Bif_sf.
         pose s' := fun _ : nat => s.
         move => isf.
         apply (mk_Bif s s').
-            exact ι.
             unfold s' => _; exact isf.
             move => x; apply lim_seq_cte.
             unfold s'; unfold fun_norm;
@@ -498,12 +490,11 @@ Section Bif_op.
     Definition Bif_plus {f g : X -> E} (bf : Bif μ f) (bg : Bif μ g) :
         Bif μ (f + g)%fn.
     (*Definition*)
-        case: bf => sf ι isf Hfpw Hfl1;
-        case: bg => sg _ isg Hgpw Hgl1.
+        case: bf => sf isf Hfpw Hfl1;
+        case: bg => sg isg Hgpw Hgl1.
         assert (∀ n : nat, integrable_sf μ (sf n + sg n)%sf) as isfplusg.
             move => n; apply integrable_sf_plus; [apply isf | apply isg].
         apply: (mk_Bif (f + g)%fn (fun n : nat => sf n + sg n)%sf).
-            exact ι.
             exact isfplusg.
             move => x; unfold fun_plus.
             apply (lim_seq_ext (fun n => sf n x + sg n x)%hy).
@@ -563,7 +554,6 @@ Section Bif_op.
         rewrite (LInt_p_ext _ _ (λ x : X, Rbar_plus ((‖ f - sf n ‖)%fn x) ((‖ g - sg n ‖)%fn x)%hy)).
             2 : by [].
         rewrite LInt_p_plus.
-            2 : exact ι.
             2, 3 : split.
             2, 4 : unfold sum_Rbar_nonneg.nonneg => x.
             2, 3 : unfold fun_norm; apply norm_ge_0.
@@ -644,9 +634,8 @@ Section Bif_op.
 
     Definition Bif_scal {f : X -> E} (a : R_AbsRing) (bf : Bif μ f) : Bif μ (a ⋅ f)%fn.
     (* Definition *)
-        case_eq bf => sf ι isf Hfpw Hfl1 Eqf.
+        case_eq bf => sf isf Hfpw Hfl1 Eqf.
         apply: (mk_Bif (a â‹… f)%fn (fun n : nat => a â‹… sf n)%sf).
-            exact ι.
             move => n; apply integrable_sf_scal; apply isf.
             move => x; unfold fun_scal.
             apply (lim_seq_ext (fun n => a â‹… sf n x)%hy).
@@ -714,9 +703,8 @@ Section Bif_op.
 
     Definition Bif_norm {f : X -> E} (bf : Bif μ f) : Bif μ (‖f‖)%fn.
     (* Definition *)
-        case_eq bf => sf ι isf Hfpw Hfl1 Eqf.
+        case_eq bf => sf isf Hfpw Hfl1 Eqf.
         apply (mk_Bif (‖f‖)%fn (fun n : nat => ‖ sf n ‖)%sf).
-            exact ι.
             move => n; apply integrable_sf_norm; apply isf.
             move => x; unfold fun_norm.
             apply (lim_seq_ext (fun n => ‖ sf n x ‖ )%hy).
@@ -797,7 +785,6 @@ Module Bif_adapted_seq.
         (* Un espace mesuré *)
         Context {gen : (X -> Prop) -> Prop}.
         Context {μ : measure gen}.
-        Context (ι : inhabited X).
         Context {f : X -> E}.
         Context (Hmeas : measurable_fun gen open f).
 
@@ -1511,11 +1498,9 @@ Module Bif_adapted_seq.
         Proof.
             move => n.
             apply: finite_LInt_p_integrable_sf.
-            exact ι.
             move => k Hk.
             apply: s_nz => //.
             rewrite <-LInt_p_SFp_eq.
-            2 : exact ι.
             2 : unfold sum_Rbar_nonneg.nonneg => x /=.
             2 : rewrite fun_sf_norm; apply norm_ge_0.
             apply Rbar_bounded_is_finite with 0%R (Rbar_mult 2 (LInt_p μ (λ x : X, (‖ f ‖)%fn x))) => //.
@@ -1686,7 +1671,7 @@ Module Bif_adapted_seq.
                 assumption.
 
             pose HCVD := LInt_p_dominated_convergence
-                              ι μ
+                              μ
                 (fun n => (λ x : X, (‖ f - s n ‖)%fn x))
                 (fun x : X => 3 * ‖ f x ‖)
                 H1_CVD
@@ -1733,7 +1718,7 @@ Module Bif_adapted_seq.
         Proof.
             exact
             (mk_Bif f s
-            ι s_integrable_sf
+            s_integrable_sf
             s_pointwise_cv s_l1_cv).
         Qed.
 
@@ -1756,12 +1741,10 @@ Section R_valued_Bif.
     Lemma R_Bif {f : X -> R_NormedModule} :
         measurable_fun gen open f ->
         is_finite (LInt_p μ (‖f‖)%fn) ->
-        inhabited X ->
             Bif μ f.
     Proof.
-        move => Hmeas Hfin ι.
+        move => Hmeas Hfin.
         apply Bif_separable_range with (fun n => Q2R (bij_NQ n)).
-        exact ι.
         exact Hmeas.
         assert (∀ x : R_NormedModule, inRange f x -> True)
             as Hle.
@@ -1774,9 +1757,8 @@ Section R_valued_Bif.
     Lemma R_bif_fun
         {f : X -> R_NormedModule}
         {Hmeas : measurable_fun gen open f}
-        {Hfin : is_finite (LInt_p μ (‖f‖)%fn)}
-        {ι : inhabited X} :
-        ∀ x : X, R_Bif Hmeas Hfin ι x = f x.
+        {Hfin : is_finite (LInt_p μ (‖f‖)%fn)} :
+        ∀ x : X, R_Bif Hmeas Hfin x = f x.
     Proof.
         by [].
     Qed.
@@ -1867,7 +1849,7 @@ Section strongly_measurable_fun.
     Lemma Bif_strongly_measurable {f : X -> E} :
         Bif μ f -> strongly_measurable f.
     Proof.
-        case => s ι _ H_pw _.
+        case => s _ H_pw _.
         exists s => //.
     Qed.
 
@@ -1991,10 +1973,10 @@ Section Bif_characterisation.
 
     Lemma strongly_measurable_integrable_Bif {f : X -> E}
         : strongly_measurable gen f -> is_finite (LInt_p μ (‖f‖)%fn)
-            -> inhabited X -> Bif μ f.
+             -> Bif μ f.
     Proof.
         exact
-        (fun Hmeas Hfin ι => Bif_separable_range ι
+        (fun Hmeas Hfin => Bif_separable_range
             (strongly_measurable_measurable Hmeas)
             (strongly_measurable_separated_range Hmeas)
             (Hfin)).
@@ -2002,9 +1984,9 @@ Section Bif_characterisation.
 
     Lemma strongly_measurable_integrable_Bif_correct
         {f : X -> E} {Hmeas : strongly_measurable gen f}
-        {Hfin : is_finite (LInt_p μ (‖f‖)%fn)} {ι : inhabited X}
+        {Hfin : is_finite (LInt_p μ (‖f‖)%fn)}
         : ∀ x : X, f x =
-        strongly_measurable_integrable_Bif Hmeas Hfin ι x.
+        strongly_measurable_integrable_Bif Hmeas Hfin x.
     Proof.
         by [].
     Qed.
diff --git a/Lebesgue/bochner_integral/Bsf_Lsf.v b/Lebesgue/bochner_integral/Bsf_Lsf.v
index e0c5da4c16c412832f7b83fd6c052a288f317c08..9c656c210beed24e380c30732f663a30bf14716b 100644
--- a/Lebesgue/bochner_integral/Bsf_Lsf.v
+++ b/Lebesgue/bochner_integral/Bsf_Lsf.v
@@ -767,12 +767,12 @@ Section simpl_fun_integrability.
     Qed.
 
     Lemma finite_LInt_p_integrable_sf :
-        ∀ sf : simpl_fun E gen, inhabited X ->
+        ∀ sf : simpl_fun E gen,
             (∀ k : nat, k < max_which sf -> val sf k ≠ zero)
             -> is_finite (LInt_SFp μ (‖sf‖)%sf (is_SF_Bsf μ (‖sf‖)%sf))
             -> integrable_sf μ sf.
     Proof.
-        move => sf ι.
+        move => sf.
         case_eq sf => wf vf maxf axf1 axf2 axf3 Eqf.
         rewrite <-Eqf => /=.
         move => sf_nz FinInt.
@@ -810,7 +810,6 @@ Section simpl_fun_integrability.
         apply RIneq.Rle_refl.
         rewrite <-LInt_SFp_scal.
         apply LInt_SFp_monotone.
-        exact ι.
         unfold charac, nonneg => x.
         case: (excluded_middle_informative (which sf x = k)).
         move => _ /=.
@@ -828,7 +827,6 @@ Section simpl_fun_integrability.
         replace ((‖ sf ‖)%sf x) with ((‖ sf ‖)%fn x).
         2 : unfold fun_norm; rewrite fun_sf_norm => //.
         apply H.
-        exact ι.
         unfold nonneg => x /=.
         rewrite fun_sf_norm.
         apply norm_ge_0.
diff --git a/Lebesgue/bochner_integral/simpl_fun.v b/Lebesgue/bochner_integral/simpl_fun.v
index e2d429df7460be769ab8a5fc701825de885c2333..9ec1fe926680888061f7508b2b2ca5a9a1f504e4 100644
--- a/Lebesgue/bochner_integral/simpl_fun.v
+++ b/Lebesgue/bochner_integral/simpl_fun.v
@@ -692,13 +692,16 @@ Section simpl_fun_bounded.
     Open Scope hy_scope.
 
     Definition sf_bounded :
-        ∀ sf : simpl_fun E gen, { M : R | ∀ x : X, ‖ fun_sf sf x ‖ <= M }.
+        ∀ sf : simpl_fun E gen, { M : R | (∀ x : X, ‖ fun_sf sf x ‖ <= M) /\ 0 <= M }.
     (* definition *)
         move => sf.
-        apply exist with (Rmax_n (fun k => ‖ val sf k ‖) (max_which sf)).
+        apply exist with (Rbasic_fun.Rmax 0 (Rmax_n (fun k => ‖ val sf k ‖) (max_which sf))).
+        split.
         move => x; unfold fun_sf.
         pose Hwx := ax_which_max_which sf x; clearbody Hwx.
+        apply Rle_trans with (2:=Rbasic_fun.Rmax_r _ _).
         apply: fo_le_Rmax_n => //.
+        apply Rbasic_fun.Rmax_l.
     Qed.
 
 End simpl_fun_bounded.
diff --git a/Lebesgue/simple_fun.v b/Lebesgue/simple_fun.v
index eea49a3abcc079c7eb9bcfc57ed790d660b3adbc..6882841e2c5e3631746f8b5ed728679bee835177 100644
--- a/Lebesgue/simple_fun.v
+++ b/Lebesgue/simple_fun.v
@@ -21,7 +21,7 @@ COPYING file for more details.
 
  Some proof paths may differ. *)
 
-From Coq Require Import ClassicalDescription.
+From Coq Require Import ClassicalDescription ClassicalEpsilon.
 From Coq Require Import PropExtensionality FunctionalExtensionality.
 From Coq Require Import Lia Reals Lra List Sorted.
 From Coquelicot Require Import Coquelicot.
@@ -38,7 +38,6 @@ Require Import measure.
 Section finite_vals_def.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Definition finite_vals : (E -> R) -> list R -> Prop :=
   fun f l => forall y, In (f y) l.
@@ -50,15 +49,26 @@ Definition finite_vals_canonic : (E -> R) -> list R -> Prop :=
     (forall y, In (f y) l).
 
 Lemma finite_vals_canonic_not_nil :
-  forall f l, finite_vals_canonic f l -> l <> nil.
+  forall f l, inhabited E -> finite_vals_canonic f l -> l <> nil.
 Proof.
-intros f l (V1,(V2,V3)) V4.
+intros f l [ x ] (V1,(V2,V3)) V4.
 rewrite V4 in V3.
-inversion Einhab as [ x ].
 specialize (V3 x).
 apply (in_nil V3).
 Qed.
 
+Lemma finite_vals_canonic_nil :
+  forall f l, ~ inhabited E -> finite_vals_canonic f l -> l = nil.
+Proof.
+intros f l; case l; try easy.
+clear l; intros a l H1 H2.
+exfalso; apply H1.
+destruct H2 as (_,(Y1,_)).
+destruct (Y1 a); try easy.
+apply in_eq.
+Qed.
+
+
 Lemma finite_vals_canonic_unique :
   forall f l1 l2,
     finite_vals_canonic f l1 ->
@@ -291,7 +301,6 @@ End finite_vals_def.
 Section SF_def.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Variable gen : (E -> Prop) -> Prop.
 
@@ -316,7 +325,6 @@ End SF_def.
 Section SF_Facts.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Variable gen : (E -> Prop) -> Prop.
 
@@ -351,7 +359,6 @@ End SF_Facts.
 Section LInt_SFp_def.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.
 Variable mu : measure gen.
@@ -387,6 +394,7 @@ Qed.
 Definition LInt_SFp : forall (f : E -> R), SF gen f -> Rbar :=
   fun f H => let l := proj1_sig H in sum_Rbar_map l (af1 f).
 
+
 Lemma LInt_SFp_correct :
   forall f (H1 H2 : SF gen f), nonneg f -> LInt_SFp f H1 = LInt_SFp f H2.
 Proof.
@@ -413,9 +421,30 @@ apply LInt_SFp_correct; try easy.
 now rewrite <- H.
 Qed.
 
-Lemma SF_cst : forall (x : E) a, SF gen (fun _ => a).
+Lemma LInt_SFp_ext_ex :
+  forall f1 (H1 : SF gen f1) f2,
+    nonneg f1 ->
+    (forall x, f1 x = f2 x) ->
+     exists (H2 : SF gen f2),
+        LInt_SFp f1 H1 = LInt_SFp f2 H2.
+Proof.
+intros f1 H1 f2 H2 H3.
+assert (T:f1 = f2).
+now apply functional_extensionality.
+generalize H1; intros H4.
+rewrite T in H1.
+exists H1.
+apply LInt_SFp_ext; easy.
+Qed.
+
+
+Lemma SF_cst : forall a, SF gen (fun _ => a).
 Proof.
-intros t a; exists (a :: nil).
+intros a.
+case (excluded_middle_informative ((exists t:E, True)) ); intros Z.
+apply constructive_indefinite_description in Z.
+destruct Z as [ t _ ].
+exists (a :: nil).
 split.
 split.
 apply LSorted_cons1.
@@ -430,16 +459,28 @@ apply measurable_ext with (fun _ => True); try easy.
 apply measurable_full.
 apply measurable_ext with (fun _ => False); try easy.
 apply measurable_empty.
+(* *)
+exists nil; split; try split; try split.
+apply LSorted_nil.
+intros; easy.
+intros t; contradict Z; easy.
+intros b; apply measurable_ext with (2:=measurable_empty gen).
+intros t; contradict Z; easy.
 Defined.
 
-Lemma LInt_SFp_0 : forall x, LInt_SFp (fun _ => 0) (SF_cst x 0) = 0.
+Lemma LInt_SFp_0 : LInt_SFp (fun _ => 0) (SF_cst 0) = 0.
 Proof.
-intros x; unfold SF_cst, LInt_SFp; simpl.
-unfold af1, sum_Rbar_map; simpl.
+unfold SF_cst, LInt_SFp; simpl.
+case (excluded_middle_informative (exists _ : E, True)); simpl.
+intros (t,Ht); simpl.
+case (constructive_indefinite_description _); simpl.
+intros _ _ ; unfold af1, sum_Rbar_map; simpl.
 rewrite Rbar_mult_0_l.
 apply Rbar_plus_0_l.
+intros H; unfold sum_Rbar_map; simpl; easy.
 Qed.
 
+
 (* Lemma 759 p. 153 *)
 Lemma SF_aux_measurable :
   forall f l, SF_aux gen f l -> measurable_fun gen gen_R f.
@@ -552,6 +593,9 @@ Lemma SFp_decomp_aux :
       sum_Rbar_map lg (fun z => mu (fun x => f x = y /\ g x = z)).
 Proof.
 intros f g lf lg y Hf Hg Hy.
+assert (Z: inhabited E).
+destruct Hf as ((_,(Y1,_)),_).
+destruct (Y1 y Hy) as (t,Ht); easy.
 assert (length lg <> 0)%nat.
 intros K; cut (lg = nil).
 apply finite_vals_canonic_not_nil with g; try easy.
@@ -982,13 +1026,10 @@ apply LInt_SFp_scal_aux; easy.
  (* a = 0 *)
 intros J3; rewrite <- J3 at 1.
 rewrite Rbar_mult_0_l.
-destruct Einhab.
-rewrite <- (LInt_SFp_0 X).
+rewrite <- LInt_SFp_0.
 apply LInt_SFp_ext; try easy.
-intros y.
-rewrite <- J3, Rmult_0_l.
-apply Rbar_le_refl.
-intros y; rewrite <- J3; apply Rmult_0_l.
+intros t; rewrite <- J3, Rmult_0_l; apply Rle_refl.
+intros t; rewrite <- J3; ring.
 Qed.
 
 (* Lemma 781 p. 160 *)
@@ -1068,7 +1109,8 @@ intros A HA.
 unfold LInt_SFp; simpl.
 rewrite canonizer_Sorted; try easy.
 unfold RemoveUseless; simpl.
-case (excluded_middle_informative _); case (excluded_middle_informative _); intros Y1 Y2;
+case (ClassicalDescription.excluded_middle_informative _); 
+  case (ClassicalDescription.excluded_middle_informative _); intros Y1 Y2;
   unfold sum_Rbar_map; simpl; unfold af1.
 rewrite Rbar_mult_0_l, Rbar_plus_0_l.
 rewrite Rbar_mult_1_l, Rbar_plus_0_r.
@@ -1219,10 +1261,10 @@ apply measurable_compl_rev; easy.
 Defined.
 
 Lemma SF_scal_charac :
-  forall (x : E) a A, measurable gen A -> SF gen (fun t => a * charac A t).
+  forall a A, measurable gen A -> SF gen (fun t => a * charac A t).
 Proof.
-intros x a A HA; apply SF_mult_charac; try easy.
-apply (SF_cst x).
+intros a A HA; apply SF_mult_charac; try easy.
+apply SF_cst.
 Qed.
 
 Lemma SF_mult_charac_alt:
@@ -1788,7 +1830,6 @@ End Adap_seq_mk.
 Section LIntSF_Dirac.
 
 Context {E : Type}.
-Hypothesis Einhab : inhabited E.
 
 Context {gen : (E -> Prop) -> Prop}.