dsimp [BoxdotTranslation]
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! (~~p✝ ⟶ p✝)ᵇ
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ