Theorem: PropositionalLogic.HilbertSystem.stronger (PropositionalLogic/HilbertSystem/HPK.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
⊢ HPJ L → HPK L
Tactic:
admit
State after:
no goals