rcases hp with (hK | hFour)
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : p✝ ∈ Ax(𝐊𝟒(𝐋))
⊢ 𝐊𝟒(𝐇) ⊢! p✝
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐇) ⊢! p✝

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒(𝐇) ⊢! p✝