dsimp [Axioms.K, BoxdotTranslation]
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐊𝟒 ⊢! Axioms.K w✝¹ w✝ᵇ
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐊𝟒 ⊢! ⊡(w✝¹ᵇ ⟶ w✝ᵇ) ⟶ ⊡w✝¹ᵇ ⟶ ⊡w✝ᵇ