cases xs
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ xs.join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = xs.join
case nil
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join

case cons
α : Type
R : RegExp α
cs head✝ : List α
tail✝ : List (List α)
a2_left : ∀ r ∈ head✝ :: tail✝, r ∈ RegExp.languageOf α R
a2_right : (head✝ :: tail✝).join = cs
⊢ (head✝ :: tail✝).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (head✝ :: tail✝).join