rw [del_star_curried, bind_eq_bind, hq', some_bind] at h
case some.mp
α 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 (x :: xs) q) = true
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1
case some.mp
α 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
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1