{α₁ β₁ : Type u_1} →
  [inst : Std.Iterator α₁ Id β₁] →
    {it₁ : Std.Iter β₁} →
      (motive : it₁.Step → Sort u_2) →
        (x : it₁.Step) →
          ((it₁' : Std.Iter β₁) →
              (out : β₁) →
                (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩) →
            ((it₁' : Std.Iter β₁) →
                (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩) →
              ((hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩) → motive x