case epsilon =>
  simp only [RegExp.is_nullable]
  simp only [RegExp.languageOf]
  simp
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if RegExp.epsilon.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
no goals