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