apply RunFromRestricted_final
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFARunToRun r✝) ⋯) ∈ (fromNFA M).F
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun r✝) ∈ (fromNFA M).F