. obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, BoxdotTranslation]; apply boxdot_axiomK!;
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ