simp only [r_ih]
α : 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 ∅
⊢ {x | ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α s.delta, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
α : 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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ RegExp.languageOf α s.delta, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅