{α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {motive : MeasureTheory.IsProbabilityMeasure μ → Sort u} →
        ((measure_univ : μ Set.univ = 1) → motive ⋯) → (t : MeasureTheory.IsProbabilityMeasure μ) → motive t