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
⊢ ∅ ⊆ Γ
Tactic:
simp
State after:
no goals