dsimp [BoxdotTranslation]
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝ᵇ
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝