induction e
α : Type
e : RegExp α
⊢ e.is_nullable ↔ [] ∈ RegExp.languageOf α e
case char
α : Type
a✝ : α
⊢ (RegExp.char a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.char a✝)

case epsilon
α : Type
⊢ RegExp.epsilon.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.epsilon

case zero
α : Type
⊢ RegExp.zero.is_nullable ↔ [] ∈ RegExp.languageOf α RegExp.zero

case union
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ : a✝¹.is_nullable ↔ [] ∈ RegExp.languageOf α a✝¹
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ (a✝¹.union a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (a✝¹.union a✝)

case concat
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ : a✝¹.is_nullable ↔ [] ∈ RegExp.languageOf α a✝¹
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ (a✝¹.concat a✝).is_nullable ↔ [] ∈ RegExp.languageOf α (a✝¹.concat a✝)

case closure
α : Type
a✝ : RegExp α
a_ih✝ : a✝.is_nullable ↔ [] ∈ RegExp.languageOf α a✝
⊢ a✝.closure.is_nullable ↔ [] ∈ RegExp.languageOf α a✝.closure