subst_vars
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! Axioms.Four w✝ᵇ