induction p using Superintuitionistic.Formula.rec' with
| hatom => simp only [GoedelTranslation.atom_def, axiomFour!];
| himp => simp only [GoedelTranslation.imp_def, axiomFour!];
| hfalsum => simp only [GoedelTranslation.falsum_def, efq!];
| hverum => exact dhyp! (nec! verum!);
| hand p q ihp ihq =>
  simp only [GoedelTranslation.and_def];
  exact imp_trans! (andReplace! ihp ihq) collect_box_and!
| hor p q ihp ihq =>
  simp only [GoedelTranslation.or_def];
  exact imp_trans! (disj₃''! (implyOrLeft'! ihp) (implyOrRight'! ihq)) collect_box_or!
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! pᵍ ⟶ □pᵍ
no goals