Theorem: ClassicalPropositionalLogic.deduction_theorem (GlimpseOfLean/Exercises/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
sorry
State after:
no goals