simp only [RegExp.languageOf]
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ {[]}