tauto
case h
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
⊢ r.is_nullable ∧ cs = [] ∨ s.is_nullable ∧ cs = [] ↔ (r.is_nullable ∨ s.is_nullable) ∧ cs = []
no goals