. obtain ⟨_, e⟩ := hFour; subst_vars; dsimp [Axioms.Four, BoxdotTranslation]; apply boxdot_axiomFour!;
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
no goals