simp only [RegExp.is_nullable]
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ True ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}