cases a2
α : Type
R : RegExp α
cs xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
case intro
α : Type
R : RegExp α
cs xs : List α
left✝ : xs ∈ RegExp.languageOf α R
right✝ : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs