{α : Type u_4} →
  {motive : MeasurableSpace.DynkinSystem α → Sort u} →
    (t : MeasurableSpace.DynkinSystem α) →
      ((Has : Set α → Prop) →
          (has_empty : Has ∅) →
            (has_compl : ∀ {a : Set α}, Has a → Has aᶜ) →
              (has_iUnion_nat :
                  ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)) →
                motive
                  { Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat }) →
        motive t