simp [IH, epsilon_closure_iff, eval_one_no_eps_iff]
case cons
α σ : 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 ∈ M.eval_from (M.eval_one_no_eps (M.epsilon_closure S) a) as, s ∈ M.accepting_state_list) ↔
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)
case cons
α σ : 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,
      (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
        M.toAbstract.eval s as) ↔
    ∃ s ∈ S, M.toAbstract.eval s (a :: as)