{Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : PartialOrder ι] →
        {𝓕 : MeasureTheory.Filtration ι m} →
          {motive : 𝓕.IsRightContinuous → Sort u} →
            (t : 𝓕.IsRightContinuous) → ((RC : 𝓕.rightCont ≤ 𝓕) → motive ⋯) → motive t