rcases a with (hK | hVer)
case mp.hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a : p✝ ∈ Ax(𝐕𝐞𝐫)
h : 𝐕𝐞𝐫 ⊢! p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
case mp.hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case mp.hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐕𝐞𝐫 ⊢! p✝
hVer : p✝ ∈ 𝗩𝗲𝗿
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯