induction p using Formula.rec' with
| hand p q ihp ihq => dsimp [BoxdotTranslation]; exact and_replace_iff! ihp ihq;
| hor p q ihp ihq => dsimp [BoxdotTranslation]; exact or_replace_iff! ihp ihq;
| himp p q ihp ihq => dsimp [BoxdotTranslation]; exact imp_replace_iff! ihp ihq;
| hbox p ihp =>
  dsimp [BoxdotTranslation];
  exact iff_trans! (box_iff! ihp) iff_box_boxdot!;
| _ => dsimp [BoxdotTranslation]; exact iff_id!;
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p ⟷ pᵇ
no goals