Missed.

Lebesgue/bochner_integral/BInt_LInt_p.v

@@ -391,7 +391,7 @@ Section BInt_to_LInt_p.
         rewrite Raxioms.Rplus_0_l in Hn'.
         simpl in Hn'; clear HN.
         unfold minus.
-        rewrite BInt_sf_LInt_SFp.
+        rewrite BInt_sf_LInt_SF.
         all : swap 1 2.
         apply integrable_sf_plus.
         apply isf.
@@ -448,7 +448,7 @@ Section BInt_to_LInt_p.
         replace (LInt_p μ (λ x : X, (sf n + ss)%sf x)) with
             (Finite (BInt_sf μ (sf n + ss)%sf)).
         easy.
-        rewrite Finite_BInt_sf_LInt_SFp.
+        rewrite Finite_BInt_sf_LInt_SF.
         rewrite <-LInt_p_SFp_eq => //.
         move => x /=.
         rewrite Eqss.
@@ -474,7 +474,7 @@ Section BInt_to_LInt_p.
         replace (LInt_p μ (λ x : X, (ss)%sf x)) with
             (Finite (BInt_sf μ (ss)%sf)).
         easy.
-        rewrite Finite_BInt_sf_LInt_SFp.
+        rewrite Finite_BInt_sf_LInt_SF.
         rewrite <-LInt_p_SFp_eq => //.
         move => x.
         rewrite Eqss /=.