simp
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = l} ↔
    cs ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α R,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = l}, r ++ s = x}
case h
α : Type
R : RegExp α
cs : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs) ↔
    cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs