dsimp [BoxdotTranslation]
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ (p ⋏ q)ᵇ
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ pᵇ ⋏ qᵇ