case _ a2_left a2_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    apply Exists.intro ([xs] ++ ys)
    simp
    tauto
α : 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
no goals