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

State before:
L : Type u
inst✝⁷ : DecidableEq L
inst✝⁶ : HilbertSystem L
inst✝⁵ : HasBot L
inst✝⁴ : HasArrow L
inst✝³ : HasLnot L
inst✝² : HasLor L
inst✝¹ : HasLand L
inst✝ : HasLiff L
Γ : Context L
φ : L
⊢ (HPM₀ L → (Γ ⊢ φ)) → HPM L → (Γ ⊢ φ)
Tactic:
admit
State after:
no goals