ext 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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} =
    if r.is_nullable ∧ s.is_nullable then {[]} else ∅
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 α
⊢ cs ∈ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} ↔
    cs ∈ if r.is_nullable ∧ s.is_nullable then {[]} else ∅