have ⟨r', _, _⟩ := h
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)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
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)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
r' : NFA.Run (toNFA M) q' xs
left✝ : constrRun xs q' = some r'
right✝ : NFA.Run.step q ⋯ r' ⋯ = r
⊢ ∃ a, constrRun xs q' = some a