Theorem: LO.Modal.Standard.Formula.VerTranslation.back (Logic/Modal/Standard/Maximal.lean)

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

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

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