Theorem: nullable_star (Katydid/Conal/Calculus.lean)

State before:
α : Type u_1
⊢ (P : dLang α) → ν' (P*) ≃ List (ν' P)
Tactic:
sorry
State after:
no goals