. assumption
case val.d.hlast
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.run
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀ : q₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) q₀ w
no goals