simp [VerTranslation, toPropFormula, Superintuitionistic.Formula.toModalFormula]
case hbox
α : Sort ?u.44261
inst✝ : DecidableEq α
α✝ : Type u_1
p✝ : Formula α✝
a✝ : (p✝ⱽᴾ) ⋯ᴹ = p✝ⱽ
⊢ ((□p✝)ⱽᴾ) ⋯ᴹ = (□p✝)ⱽ
no goals