ext cs
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
⊢ N.to_DFA.accepts = N.accepts
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.accepts cs ↔ N.accepts cs