{α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {motive : MeasureTheory.NoAtoms μ → Sort u} →
        (t : MeasureTheory.NoAtoms μ) → ((measure_singleton : ∀ (x : α), μ {x} = 0) → motive ⋯) → motive t