{α : Type u} →
  {f : α → α} →
    {motive : Std.Iterators.Types.RepeatIterator α f → Sort u_1} →
      (t : Std.Iterators.Types.RepeatIterator α f) → ((next : α) → motive { next := next }) → motive t