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