simp only [s_ih]
α : 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
no goals