simp only [r_ih]
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ r.is_nullable ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∨ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∨ [] ∈ RegExp.languageOf α s