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

State before:
α : Type u_1
⊢ (a : α) → (P : dLang α) → δ' (P*) a ≡ (List (ν' P) · δ' P a , P*)
Tactic:
sorry
State after:
no goals