split_ifs
α : 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)
case pos
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
h✝ : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)

case neg
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
h✝ : ¬a = b
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)