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

State before:
α : Type u_1
⊢ (a : α) → δ' ε a ≡ ∅
Tactic:
sorry
State after:
no goals