simp only [RegExp.languageOf] at r_ih
α : Type
r s : RegExp α
r_ih :
  RegExp.languageOf α r.delta =
    if r.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
α : Type
r s : RegExp α
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero