∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} {steps : ℕ}
  {evals_in_steps : (flip bind f)^[steps] (some a) = b} {steps_1 : ℕ}
  {evals_in_steps_1 : (flip bind f)^[steps_1] (some a) = b},
  { steps := steps, evals_in_steps := evals_in_steps } = { steps := steps_1, evals_in_steps := evals_in_steps_1 } →
    steps = steps_1