have : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) := by_axm! (by simp)
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ
case b
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
this✝ : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ
this : [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! pᵍ ⟶ □(qᵍ ⟶ rᵍ)
⊢ [pᵍ, pᵍ ⟶ □(qᵍ ⟶ rᵍ)] ⊢[m𝓓]! qᵍ ⟶ rᵍ