simp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈
      {x |
        ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e),
          ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x} ↔
    a :: w ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w) ↔
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w