intro xs a2
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α (RegExp.derivative a e) ∧
        ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ a_1 ++ a.join = w) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a e) ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w