∀ {α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m β] (it₂ : Std.IterM m β)
  (motive : it₂.Step → Sort u_3) (it₂' : Std.IterM m β) (out : β)
  (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out))
  (h_1 :
    (it₂' : Std.IterM m β) →
      (out : β) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m β) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₂' out, h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₂' out h