∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {motive : (step : Std.IterStep (Std.IterM m β) β) → Std.Iterators.Types.Take.PlausibleStep it step → Prop},
  (∀ {it' : Std.IterM m β} {out : β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
      (h : it.internalState.countdown ≠ 1),
      motive
        (Std.IterStep.yield
          { internalState := { countdown := it.internalState.countdown - 1, inner := it', finite := ⋯ } } out)
        ⋯) →
    (∀ {it' : Std.IterM m β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
        (a_1 : it.internalState.countdown ≠ 1),
        motive
          (Std.IterStep.skip
            { internalState := { countdown := it.internalState.countdown, inner := it', finite := ⋯ } })
          ⋯) →
      (∀ (a : it.internalState.inner.IsPlausibleStep Std.IterStep.done), motive Std.IterStep.done ⋯) →
        (∀ (a : it.internalState.countdown = 1), motive Std.IterStep.done ⋯) →
          ∀ {step : Std.IterStep (Std.IterM m β) β} (t : Std.Iterators.Types.Take.PlausibleStep it step), motive step t