∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  [inst_1 : Std.Iterators.Productive α m] (motive : Std.IterM m β → Sort x)
  (step :
    (it : Std.IterM m β) →
      ({it' : Std.IterM m β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it)
  (it : Std.IterM m β),
  Std.IterM.inductSkips motive step it = step it fun {it'} x => Std.IterM.inductSkips motive step it'