∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β) (P : β → Prop),
  (∀ (b : β), it.IsPlausibleIndirectOutput b → P b) →
    ∀ (it' : Std.IterM m β) (out : β), it.IsPlausibleStep (Std.IterStep.yield it' out) → P out