Theorem: LO.Modal.Standard.S4_of_boxdotTranslatedK4 (Logic/Modal/Standard/Boxdot.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! pᵇ
⊢ 𝐒𝟒 ⊢! p
Tactic:
exact (conj₂'! iff_boxdotTranslation_S4) ⨀ (reducible_iff.mp $ reducible_K4_S4) h
State after:
no goals