obtain ⟨_, _, e⟩ := hK
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒𝐇 ⊢! p✝
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒𝐇 ⊢! p✝