simp only [GoedelTranslation.imp_def, axiomFour!]
case himp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p✝ q✝ : Superintuitionistic.Formula α
a✝¹ : m𝓓 ⊢! p✝ᵍ ⟶ □p✝ᵍ
a✝ : m𝓓 ⊢! q✝ᵍ ⟶ □q✝ᵍ
⊢ m𝓓 ⊢! (p✝ ⟶ q✝)ᵍ ⟶ □(p✝ ⟶ q✝)ᵍ
no goals