simp
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (∀ r ∈ [xs] ++ ys, r ∈ RegExp.languageOf α R) ∧ ([xs] ++ ys).join = cs
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (xs ∈ RegExp.languageOf α R ∧ ∀ a ∈ ys, a ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs