simp [last]
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G (RegularDerivation.step x✝ v'✝ h✝ h_w✝ a✝)) ∈ (toNFA G).F
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G a✝) ∈ (toNFA G).F