{α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {motive : Std.Iterators.Finite α m → Sort u} →
          ((wf : WellFounded Std.IterM.IsPlausibleSuccessorOf) → motive ⋯) → (t : Std.Iterators.Finite α m) → motive t