simpa using ihpq ⟨hpq⟩
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ q✝ : Superintuitionistic.Formula α
hpq : Superintuitionistic.Deduction 𝐈𝐧𝐭 (p✝ ⟶ q✝)
hp : Superintuitionistic.Deduction 𝐈𝐧𝐭 p✝
ihpq : 𝐈𝐧𝐭 ⊢! p✝ ⟶ q✝ → 𝐒𝟒 ⊢! (p✝ ⟶ q✝)ᵍ
ihp : 𝐈𝐧𝐭 ⊢! p✝ → 𝐒𝟒 ⊢! p✝ᵍ
h : 𝐈𝐧𝐭 ⊢! q✝
⊢ 𝐒𝟒 ⊢! □(p✝ᵍ ⟶ q✝ᵍ)
no goals