Theorem: PropositionalLogic.HilbertSystem.HPM₀.weakenContext (PropositionalLogic/HilbertSystem/HPM₀.lean)

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
Γ Δ : Context L
hs : Γ ⊆ Δ
⊢ (Γ ⊢ φ) → (Δ ⊢ φ)
Tactic:
sorry
State after:
no goals