simp only [RegExp.languageOf]
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ ∅ ↔ a :: w ∈ {[b]}