simp_all only [Set.mem_setOf_eq]
case eaxm
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ : Superintuitionistic.Formula α
ih : p✝ ∈ Ax(𝐈𝐧𝐭)
h : 𝐈𝐧𝐭 ⊢! p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ
case eaxm
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r p✝ : Superintuitionistic.Formula α
ih : ∃ p, Axioms.EFQ p = p✝
h : 𝐈𝐧𝐭 ⊢! p✝
⊢ 𝐒𝟒 ⊢! p✝ᵍ