induction e generalizing w
α : Type
inst✝ : DecidableEq α
a : α
w : List α
e : RegExp α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
case char
α : Type
inst✝ : DecidableEq α
a a✝ : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (RegExp.char a✝)) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char a✝)

case epsilon
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.epsilon) ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon

case zero
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α RegExp.zero

case union
α : Type
inst✝ : DecidableEq α
a : α
a✝¹ a✝ : RegExp α
a_ih✝¹ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝¹) ↔ a :: w ∈ RegExp.languageOf α a✝¹
a_ih✝ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝) ↔ a :: w ∈ RegExp.languageOf α a✝
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (a✝¹.union a✝)) ↔ a :: w ∈ RegExp.languageOf α (a✝¹.union a✝)

case concat
α : Type
inst✝ : DecidableEq α
a : α
a✝¹ a✝ : RegExp α
a_ih✝¹ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝¹) ↔ a :: w ∈ RegExp.languageOf α a✝¹
a_ih✝ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝) ↔ a :: w ∈ RegExp.languageOf α a✝
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (a✝¹.concat a✝)) ↔ a :: w ∈ RegExp.languageOf α (a✝¹.concat a✝)

case closure
α : Type
inst✝ : DecidableEq α
a : α
a✝ : RegExp α
a_ih✝ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝) ↔ a :: w ∈ RegExp.languageOf α a✝
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a a✝.closure) ↔ a :: w ∈ RegExp.languageOf α a✝.closure