simp only [RegExp.languageOf]
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ RegExp.languageOf α R.closure ↔ cs ∈ RegExp.languageOf α (RegExp.epsilon.union (R.concat R.closure))
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}