refine nec! $ imp_trans! (imp_trans! (axiomK'! $ nec! ?b) axiomFour!) $ axiomK'! $ nec! $ imp_trans! (axiomK'! $ nec! imply₂!) axiomK!
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ □(□(pᵍ ⟶ qᵍ) ⟶ □(pᵍ ⟶ 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𝓓
⊢ m𝓓 ⊢! (pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ pᵍ ⟶ qᵍ ⟶ rᵍ