simp only [a3_left_right] at a3_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 xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] ++ ys = cs
⊢ (True ∧ True) ∧ cs = []
α : 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 xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] ++ [] = cs
⊢ (True ∧ True) ∧ cs = []