simp [bind_eq_bind]
case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ constrRun xs q' = some r'