assumption
case none
α 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 }
hq' : M.δ (q, x) = none
⊢ M.δ (q, x) = none

case none
α 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 }
hq' : M.δ (q, x) = none
⊢ ∀ (a : { x // x ∈ M.Q }) (H : a ∈ M.δ (q, x)),
    (do
          let r' ← constrRun xs a
          some (NFA.Run.step q ⋯ r' ⋯)) =
        none →
      M.δ (q, x) = none
case none
α 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 }
hq' : M.δ (q, x) = none
⊢ ∀ (a : { x // x ∈ M.Q }) (H : a ∈ M.δ (q, x)),
    (do
          let r' ← constrRun xs a
          some (NFA.Run.step q ⋯ r' ⋯)) =
        none →
      M.δ (q, x) = none