intro h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
⊢ ¬𝐈𝐧𝐭 ⊢! p → ¬𝐒𝟒 ⊢! pᵍ
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h : ¬𝐈𝐧𝐭 ⊢! p
⊢ ¬𝐒𝟒 ⊢! pᵍ