∀ {Ω : Type u_1} (m' m'_1 : MeasurableSpace Ω) (e_m' : m' = m'_1) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s s_1 : Set Ω),
  s = s_1 →
    ∀ (t t_1 : Set Ω),
      t = t_1 →
        ∀ (μ μ_1 : MeasureTheory.Measure Ω) (e_μ : μ = μ_1) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
          ProbabilityTheory.CondIndepSet m' hm' s t μ = ProbabilityTheory.CondIndepSet m'_1 ⋯ s_1 t_1 μ_1