∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {nextIdx n : ℕ} {inner : Std.IterM m β} {nextIdx_1 n_1 : ℕ}
  {inner_1 : Std.IterM m β},
  { nextIdx := nextIdx, n := n, inner := inner } = { nextIdx := nextIdx_1, n := n_1, inner := inner_1 } →
    nextIdx = nextIdx_1 ∧ n = n_1 ∧ inner = inner_1