simp only [a2_right]
α : 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 α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ [] = cs
no goals