∀ {m : Type u_2 → Type u_3} {α β : Type u_2} [inst : Std.Iterator α m β] {γ : Type u_1}
  (Pl : β → γ → ForInStep γ → Prop) {P : β → Prop} (it : Std.IterM m β) (init : γ)
  (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b) (out : β)
  (motive : Subtype (Pl out ⟨it, ⟨init, hP⟩⟩.snd.fst) → Prop) (forInStep : Subtype (Pl out ⟨it, ⟨init, hP⟩⟩.snd.fst)),
  (∀ (c : γ) (h : Pl out ⟨it, ⟨init, hP⟩⟩.snd.fst (ForInStep.yield c)), motive ⟨ForInStep.yield c, h⟩) →
    (∀ (c : γ) (h : Pl out ⟨it, ⟨init, hP⟩⟩.snd.fst (ForInStep.done c)), motive ⟨ForInStep.done c, h⟩) →
      motive forInStep