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