∀ {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_3}
  {𝓧 : (i : S) → T i → Type u_4} [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)]
  {X : (i : S) → (j : T i) → Ω → 𝓧 i j},
  (∀ (i : S) (j : T i), Measurable (X i j)) →
    (∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), ProbabilityTheory.iIndepFun (fun i ω j => X (↑i) (↑j) ω) P) →
      ProbabilityTheory.iIndepFun (fun i ω j => X i j ω) P