case closure e _ =>
  simp only [equiv_language_of_closure]
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α e.closure
no goals