simp only [RegExp.derivative]
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (RegExp.char b)) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (if a = b then RegExp.epsilon else RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)