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

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hH : p ∈ 𝗛
⊢ 𝐆𝐋 ⊢! p