exact .eps _ _ _ ih h
case cons.mp.head
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s₁ s₂ s₃ : σ
h3 : M.toAbstract.symbol s₂ a s₁
h4 : M.toAbstract.eval s₁ as
a✝ c✝ : σ
h : M.toAbstract.epsilon a✝ c✝
h✝ : Relation.ReflTransGen M.toAbstract.epsilon c✝ s₂
ih : M.toAbstract.eval c✝ (a :: as)
⊢ M.toAbstract.eval a✝ (a :: as)
no goals