case pos c1 =>
  simp only [c1]
  simp only [RegExp.languageOf]
  simp
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
no goals