∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (it' : Std.IterM n α)
  (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')),
  m.modifyStep it ⟨Std.IterStep.skip it', property⟩ =
    Std.IterStep.skip
      {
        internalState :=
          have __src := it.internalState;
          { inner := it', state := __src.state } }