induction h.some with
| eaxm ih =>
  simp_all only [Set.mem_setOf_eq];
  obtain ⟨p, hp⟩ := ih; subst hp;
  exact nec! efq!;
| mdp hpq hp ihpq ihp =>
  exact axiomT'! $ axiomK''! (by simpa using ihpq ⟨hpq⟩) $ nec! $ ihp ⟨hp⟩;
| verum => apply verum!;
| imply₁ => exact case_imply₁;
| imply₂ => exact case_imply₂;
| conj₁ => simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]; exact nec! conj₁!;
| conj₂ => simp only [GoedelTranslation.imp_def, GoedelTranslation.and_def]; exact nec! conj₂!;
| conj₃ => exact case_conj₃;
| disj₁ => simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]; exact nec! disj₁!;
| disj₂ => simp only [GoedelTranslation.imp_def, GoedelTranslation.or_def]; exact nec! disj₂!;
| disj₃ => exact case_disj₃;
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p
⊢ 𝐒𝟒 ⊢! pᵍ
no goals