case _ right =>
  apply Exists.elim right
  intro xs a2
  clear right
  cases a2
  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 : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
no goals