simp [TrivTranslation]
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ (□p)ᵀ
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ pᵀ