case concat r s r_ih s_ih =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
  simp only [r_ih]
  simp only [s_ih]
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ (r.concat s).is_nullable ↔ [] ∈ RegExp.languageOf α (r.concat s)
no goals