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