apply Exists.elim a2_right
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs