exact ⟨_, _, .refl, h2, h1⟩
case sym.refl
α σ : 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 : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.symbol start_state✝ a stop_state✝
h1 : M.toAbstract.eval stop_state✝ as
a_ih✝ :
  a :: as = as →
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure stop_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure start_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
no goals