apply del_star_curried_isSome_iff_constrRun_isSome.mpr
case some.mpr
α 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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M xs q'✝) = true
case some.mpr
α 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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (constrRun xs q'✝) = true