induction p using rec' with
| hbox _ => simp [VerTranslation, toPropFormula, Superintuitionistic.Formula.toModalFormula];
| _ => simp [VerTranslation, toPropFormula, Superintuitionistic.Formula.toModalFormula, *];
α : Sort ?u.44261
inst✝ : DecidableEq α
α✝ : Type u_1
p : Formula α✝
⊢ (pⱽᴾ) ⋯ᴹ = pⱽ
no goals