clear right
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = 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
α : 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