feat(Modal): Add iff_S4_boxdotTranslatedK4

[SnO2WMaN]

⊡と，論理式の□を⊡に置き換える変換ᵇを次のように定める．

-- in LogicSymbols
abbrev boxdot (p : F) : F := p ⋏ □p
prefix:74 "⊡" => boxdot

def Formula.BoxdotTranslation : Formula α → Formula α
  | atom p => .atom p
  | ⊥ => ⊥
  | p ⟶ q => (BoxdotTranslation p) ⟶ (BoxdotTranslation q)
  | p ⋏ q => (BoxdotTranslation p) ⋏ (BoxdotTranslation q)
  | p ⋎ q => (BoxdotTranslation p) ⋎ (BoxdotTranslation q)
  | box p => ⊡(BoxdotTranslation p)
postfix:75 "ᵇ" => Formula.BoxdotTranslation

このとき𝐊𝟒と𝐒𝟒について以下が成り立つ．

theorem iff_S4_boxdotTranslatedK4 : 𝐒𝟒 ⊢! p ↔ 𝐊𝟒 ⊢! pᵇ