exact run.toDerivation _ h
case val
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
no goals