simp only [RegExp.languageOf]
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.union s)
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.union s).is_nullable ↔ [] ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s