Theorem: ν (Katydid/Conal/Language.lean)

State before:
α : Type u
P : dLang α
f : Lang P
⊢ Dec (dLang.ν P)
Tactic:
induction f with
| universal => exact unit?
State after:
no goals

State before:
case universal
α : Type u
P : dLang α
⊢ Dec (dLang.ν fun x => PUnit)
Tactic:
exact unit?
State after:
no goals