subst hp
case eaxm.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝¹ q r p✝ : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! p✝
p : Superintuitionistic.Formula α
hp : Axioms.EFQ p = p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
case eaxm.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q r p : Superintuitionistic.Formula α
h : 𝐈𝐧𝐭 ⊢! Axioms.EFQ p
⊢ 𝐒𝟒 ⊢! Axioms.EFQ pᵍ