diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 741d64be4..9d260b055 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,8 +37,6 @@
   + `emeasurable_fun_sum` -> `emeasurable_sum`
   + `emeasurable_fun_fsum` -> `emeasurable_fsum`
   + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` -> `setT_setI_bigsetI`
 
 - in `classical_sets.v`:
   + `preimage_itv_o_infty` -> `preimage_itvoy`
@@ -67,6 +65,8 @@
 - in `constructive_ereal.v`
   + notation `lee_opp` (deprecated since 0.6.5)
   + notation `lte_opp` (deprecated since 0.6.5)
+- in `measure.v`:
+  + `dynkin_setI_bigsetI` (use `big_ind` instead)
 
 ### Infrastructure
 
diff --git a/theories/measure.v b/theories/measure.v
index 4f95ba626..b26b412db 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -866,14 +866,6 @@ case=> ? DC DU; split => [| |? ? ?]; last exact: DU.
 - by move=> A GA; rewrite -setTD; apply: DC.
 Qed.
 
-Lemma setT_setI_bigsetI (I0 : choiceType) (J : seq I0) G (F : I0 -> set T) :
-  G [set: T] -> setI_closed G -> (forall i, i \in J -> G (F i)) ->
-  G (\big[setI/setT]_(i <- J) F i).
-Proof.
-move=> GT GI; rewrite big_seq; elim/big_rec : _ => //.
-by move=> i A iJ ih GF; apply: GI => //; [exact: GF|exact: ih].
-Qed.
-
 Lemma dynkin_setI_sigma_algebra G : dynkin G -> setI_closed G ->
   sigma_algebra setT G.
 Proof.
@@ -883,7 +875,7 @@ move=> dG GI; split => [|//|F DF].
 - rewrite seqDU_bigcup_eq; apply/(dynkinU dG) => //.
   move=> n; rewrite /seqDU setDE; apply GI => //.
   rewrite -bigcup_mkord setC_bigcup bigcap_mkord.
-  apply: setT_setI_bigsetI => //=; first by case: dG.
+  apply: big_ind => //; first by case: dG.
   by move=> i _; exact/(dynkinC dG).
 Qed.
 
@@ -1072,7 +1064,7 @@ HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
 HB.structure Definition SemiRingOfSets d :=
   {T of Pointed T & isSemiRingOfSets d T}.
 
-Arguments measurable {d}%measure_display_scope {s} _%classical_set_scope.
+Arguments measurable {d}%_measure_display_scope {s} _%_classical_set_scope.
 
 Lemma measurable_curry (T1 T2 : Type) d (T : semiRingOfSetsType d)
     (G : T1 * T2 -> set T) (x : T1 * T2) :