induction e
α : Type
e : RegExp α
⊢ RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
case char
α : Type
a✝ : α
⊢ RegExp.languageOf α (RegExp.char a✝).delta =
    if (RegExp.char a✝).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case epsilon
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if RegExp.epsilon.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case zero
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if RegExp.zero.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case union
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ :
  RegExp.languageOf α a✝¹.delta =
    if a✝¹.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
a_ih✝ :
  RegExp.languageOf α a✝.delta =
    if a✝.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (a✝¹.union a✝).delta =
    if (a✝¹.union a✝).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case concat
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ :
  RegExp.languageOf α a✝¹.delta =
    if a✝¹.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
a_ih✝ :
  RegExp.languageOf α a✝.delta =
    if a✝.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (a✝¹.concat a✝).delta =
    if (a✝¹.concat a✝).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case closure
α : Type
a✝ : RegExp α
a_ih✝ :
  RegExp.languageOf α a✝.delta =
    if a✝.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α a✝.closure.delta =
    if a✝.closure.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero