∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive :
    (a : ℕ) →
      (a_1 : Std.IterM m β) →
        (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop}
  {motive_1 :
    {a : ℕ} →
      {a_1 : Std.IterM m β} →
        {a_2 : Std.IterStep (Std.IterM m β) β} →
          (t : Std.IterM.IsPlausibleNthOutputStep a a_1 a_2) → Std.IterM.IsPlausibleNthOutputStep.below t → Prop},
  (∀ {it' : Std.IterM m β} {out : β} {it : Std.IterM m β} (a : it.IsPlausibleStep (Std.IterStep.yield it' out)),
      motive_1 ⋯ ⋯) →
    (∀ {n : ℕ} {it : Std.IterM m β} (a : it.IsPlausibleStep Std.IterStep.done), motive_1 ⋯ ⋯) →
      (∀ {n : ℕ} {it it' : Std.IterM m β} {out : β} {step : Std.IterStep (Std.IterM m β) β}
          (a : it.IsPlausibleStep (Std.IterStep.yield it' out)) (a_1 : Std.IterM.IsPlausibleNthOutputStep n it' step)
          (ih : Std.IterM.IsPlausibleNthOutputStep.below a_1) (a_ih : motive n it' step a_1),
          motive_1 a_1 ih → motive_1 ⋯ ⋯) →
        (∀ {n : ℕ} {it it' : Std.IterM m β} {step : Std.IterStep (Std.IterM m β) β}
            (a : it.IsPlausibleStep (Std.IterStep.skip it')) (a_1 : Std.IterM.IsPlausibleNthOutputStep n it' step)
            (ih : Std.IterM.IsPlausibleNthOutputStep.below a_1) (a_ih : motive n it' step a_1),
            motive_1 a_1 ih → motive_1 ⋯ ⋯) →
          ∀ {a : ℕ} {a_1 : Std.IterM m β} {a_2 : Std.IterStep (Std.IterM m β) β}
            {t : Std.IterM.IsPlausibleNthOutputStep a a_1 a_2} (t_1 : Std.IterM.IsPlausibleNthOutputStep.below t),
            motive_1 t t_1