clear a1
case h.mp
α : 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 α
a1 : ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
xs : List α
a2 : (r.is_nullable ∧ xs = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
case h.mp
α : 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 : (r.is_nullable ∧ xs = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []