dsimp [BoxdotTranslation]
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! (□p✝)ᵇ
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! ⊡p✝ᵇ