exact .eps _ _ _ ih h
case nil.mp.head
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h3 : s ∈ M.accepting_state_list
a✝ c✝ : σ
h : M.toAbstract.epsilon a✝ c✝
h✝ : Relation.ReflTransGen M.toAbstract.epsilon c✝ s
ih : M.toAbstract.eval c✝ []
⊢ M.toAbstract.eval a✝ []
no goals