∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {P : β → Prop} {inner : Std.IterM m β}
  {invariant : ∀ (out : β), inner.IsPlausibleIndirectOutput out → P out} {inner_1 : Std.IterM m β}
  {invariant_1 : ∀ (out : β), inner_1.IsPlausibleIndirectOutput out → P out},
  { inner := inner, invariant := invariant } = { inner := inner_1, invariant := invariant_1 } → inner = inner_1