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

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