∀ {α : Type u_2} {𝒜 : Set (Set α)} {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop}
  {motive_1 :
    {a : Set α} → (t : MeasureTheory.generateSetAlgebra 𝒜 a) → MeasureTheory.generateSetAlgebra.below t → Prop}
  {a : Set α} {t : MeasureTheory.generateSetAlgebra 𝒜 a} (t_1 : MeasureTheory.generateSetAlgebra.below t),
  (∀ (s : Set α) (s_mem : s ∈ 𝒜), motive_1 ⋯ ⋯) →
    motive_1 ⋯ ⋯ →
      (∀ (s : Set α) (hs : MeasureTheory.generateSetAlgebra 𝒜 s) (ih : MeasureTheory.generateSetAlgebra.below hs)
          (hs_ih : motive s hs), motive_1 ⋯ ⋯) →
        (∀ (s t : Set α) (hs : MeasureTheory.generateSetAlgebra 𝒜 s) (ht : MeasureTheory.generateSetAlgebra 𝒜 t)
            (ih : MeasureTheory.generateSetAlgebra.below hs) (hs_ih : motive s hs)
            (ih_1 : MeasureTheory.generateSetAlgebra.below ht) (ht_ih : motive t ht), motive_1 ⋯ ⋯) →
          motive_1 t t_1