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

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐓𝐫𝐢𝐯 ⊢! p