Theorem: IntuitionisticPropositionalLogic.weakening (GlimpseOfLean/Exercises/Topics/IntuitionisticPropositionalLogic.lean)

State before:
H : Type ?u.21661
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
sorry
State after:
no goals