{α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {inst : Std.Iterator α m β} →
        {P : Sort u} →
          {nextAtIdx? nextAtIdx?' :
              (it : Std.IterM m β) → (n : ℕ) → m (Std.PlausibleIterStep (Std.IterM.IsPlausibleNthOutputStep n it))} →
            { nextAtIdx? := nextAtIdx? } = { nextAtIdx? := nextAtIdx?' } → (nextAtIdx? ≍ nextAtIdx?' → P) → P